Documentation

Matroid.ForMathlib.Topology.Summable

Additional infinite-sum lemmas #

The complete-lattice summation API is in Mathlib.Topology.Algebra.InfiniteSum.Order. This file supplements it with finite-subtype formulas, sums of piecewise functions, and criteria for a sum to equal ⊤, including the infinite-support criterion in atomic orders. It also retains the custom printers for infinite sums and products.

source
def tsum_delab :
Lean.PrettyPrinter.Delaborator.Delab

Delaborator for tsums?.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def tprod_delab :
    Lean.PrettyPrinter.Delaborator.Delab
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem tsum_subtype_eq_toFinset_sum {α : Type u_1} {M : Type u_2} {f : α → M} {s : Set α} [AddCommMonoid M] [TopologicalSpace M] (hs : s.Finite) :
      ∑' (x : ↑s), f ↑x = ∑ x ∈ hs.toFinset, f x
      source
      theorem tsum_subtype_const_of_finite {α : Type u_1} {M : Type u_2} {s : Set α} [AddCommMonoid M] [TopologicalSpace M] (hs : s.Finite) (c : M) :
      ∑' (x : ↑s), c = hs.toFinset.card • c
      source
      theorem tsum_ite {α : Type u_1} {M : Type u_2} [AddCommMonoid M] [CompleteLattice M] [CanonicallyOrderedAdd M] [TopologicalSpace M] [SupConvergenceClass M] [T2Space M] [ContinuousAdd M] (P : α → Prop) (f g : α → M) [DecidablePred P] :
      (∑' (x : α), if P x then f x else g x) = ∑' (x : ↑{x : α | P x}), f ↑x + ∑' (x : ↑{x : α | ¬P x}), g ↑x
      source
      theorem tsum_eq_top_iff_of_finite {α : Type u_1} {M : Type u_2} {f : α → M} {s : Set α} [AddCommMonoid M] [CompleteLattice M] [CanonicallyOrderedAdd M] [TopologicalSpace M] [SupConvergenceClass M] [IsOrderedAddMonoid M] [OrderClosedTopology M] [ContinuousAdd M] [AddEqTopClass M] (hs : s.Finite) :
      ∑' (x : ↑s), f ↑x = ⊤ ↔ ∃ a ∈ s, f a = ⊤
      source
      theorem tsum_const_eq_top {α : Type u_1} {M : Type u_2} [AddCommMonoid M] [TopologicalSpace M] [CompleteLinearOrder M] [SupConvergenceClass M] [CanonicallyOrderedAdd M] [AddEqTopClass M] [IsOrderedAddMonoid M] [OrderClosedTopology M] [Archimedean ↥(AddSubmonoid.neTop M)] [AddLeftStrictMono ↥(AddSubmonoid.neTop M)] [Infinite α] {c : M} (hc : c ≠ 0) :
      ∑' (x : α), c = ⊤
      source
      theorem tsum_subtype_const_eq_top {α : Type u_1} {M : Type u_2} {s : Set α} [AddCommMonoid M] [TopologicalSpace M] [CompleteLinearOrder M] [SupConvergenceClass M] [CanonicallyOrderedAdd M] [AddEqTopClass M] [IsOrderedAddMonoid M] [OrderClosedTopology M] [Archimedean ↥(AddSubmonoid.neTop M)] [AddLeftStrictMono ↥(AddSubmonoid.neTop M)] (hs : s.Infinite) {c : M} (hc : c ≠ 0) :
      ∑' (x : ↑s), c = ⊤
      source
      theorem tsum_eq_top_of_support_infinite {α : Type u_1} {M : Type u_2} {f : α → M} [AddCommMonoid M] [TopologicalSpace M] [CompleteLinearOrder M] [SupConvergenceClass M] [CanonicallyOrderedAdd M] [AddEqTopClass M] [IsOrderedAddMonoid M] [OrderClosedTopology M] [Archimedean ↥(AddSubmonoid.neTop M)] [AddLeftStrictMono ↥(AddSubmonoid.neTop M)] [IsAtomic M] (hf : (Function.support f).Infinite) :
      ∑' (a : α), f a = ⊤
      source
      theorem tsum_eq_top_iff {α : Type u_1} {M : Type u_2} {f : α → M} [AddCommMonoid M] [TopologicalSpace M] [CompleteLinearOrder M] [SupConvergenceClass M] [CanonicallyOrderedAdd M] [AddEqTopClass M] [IsOrderedAddMonoid M] [OrderClosedTopology M] [Archimedean ↥(AddSubmonoid.neTop M)] [AddLeftStrictMono ↥(AddSubmonoid.neTop M)] [IsAtomic M] :
      ∑' (a : α), f a = ⊤ ↔ (Function.support f).Infinite ∨ ∃ (a : α), f a = ⊤
      source
      theorem tsum_subtype_eq_top_iff {α : Type u_1} {M : Type u_2} {f : α → M} {s : Set α} [AddCommMonoid M] [TopologicalSpace M] [CompleteLinearOrder M] [SupConvergenceClass M] [CanonicallyOrderedAdd M] [AddEqTopClass M] [IsOrderedAddMonoid M] [OrderClosedTopology M] [Archimedean ↥(AddSubmonoid.neTop M)] [AddLeftStrictMono ↥(AddSubmonoid.neTop M)] [IsAtomic M] :
      ∑' (a : ↑s), f ↑a = ⊤ ↔ (s ∩ Function.support f).Infinite ∨ ∃ a ∈ s, f a = ⊤
      source
      theorem tsum_subtype_eq_top_of_inter_support_infinite {α : Type u_1} {M : Type u_2} {f : α → M} {s : Set α} [AddCommMonoid M] [TopologicalSpace M] [CompleteLinearOrder M] [SupConvergenceClass M] [CanonicallyOrderedAdd M] [AddEqTopClass M] [IsOrderedAddMonoid M] [OrderClosedTopology M] [Archimedean ↥(AddSubmonoid.neTop M)] [AddLeftStrictMono ↥(AddSubmonoid.neTop M)] [IsAtomic M] (hf : (s ∩ Function.support f).Infinite) :
      ∑' (a : ↑s), f ↑a = ⊤