Other results

Results named in the rest of Tau Ceti's TauCeti.Topology modules and in no roadmap's section, as Tau Ceti has them at commit ace60277.

TheoremA refined Arzelà–Ascoli theorem (Ambrosio–Gigli–Savaré, Proposition 3.3.1)#

Let l y be the filter of an auxiliary convergence y_n ⇀ y on a weak extended metric space X, for which the distance is jointly sequentially lower semicontinuous. The topology of X need not be induced by its extended distance; the auxiliary convergence is specified only by l. Let v k : T → X be maps on a separable space T such that

• at each time t, the values v k t lie in a set K t in which every sequence has a ⇀-convergent subsequence;
• limsup_k d(v k s, v k t) ≤ ω s t, where ω t s → 0 as s → t.

Then a subsequence v (ψ n) converges pointwise for ⇀ to a map u : T → X with d(u s, u t) ≤ ω s t. The maps v k need not be continuous.

TauCeti.tendsto_subseq_of_limsup_edist_le.{u_1, u_2} {T : Type u_1} {X : Type u_2}
  [TopologicalSpace T] [TopologicalSpace X] [WeakEMetricSpace X] {l : X → Filter X}
  [TopologicalSpace.SeparableSpace T]
  (hd :
    ∀ ⦃v w : ℕ → X⦄ ⦃y z : X⦄,
      Filter.Tendsto v Filter.atTop (l y) →
        Filter.Tendsto w Filter.atTop (l z) →
          edist y z ≤ Filter.liminf (fun n => edist (v n) (w n)) Filter.atTop)
  {v : ℕ → T → X} {K : T → Set X} (hvK : ∀ (k : ℕ) (t : T), v k t ∈ K t)
  (hK :
    ∀ (t : T) ⦃w : ℕ → X⦄,
      (∀ (n : ℕ), w n ∈ K t) → ∃ y ψ, StrictMono ψ ∧ Filter.Tendsto (w ∘ ψ) Filter.atTop (l y))
  {ω : T → T → ENNReal}
  (hvω : ∀ (s t : T), Filter.limsup (fun k => edist (v k s) (v k t)) Filter.atTop ≤ ω s t)
  (hω : ∀ (t : T), Filter.Tendsto (ω t) (nhds t) (nhds 0)) :
  ∃ ψ,
    StrictMono ψ ∧
      ∃ u,
        (∀ (t : T), Filter.Tendsto (fun n => v (ψ n) t) Filter.atTop (l (u t))) ∧
          ∀ (s t : T), edist (u s) (u t) ≤ ω s t

Lean

Formalized in Tau Ceti as TauCeti.tendsto_subseq_of_limsup_edist_le.

Sources

• Tau Ceti documentation: TauCeti.tendsto_subseq_of_limsup_edist_le
• Source of TauCeti.tendsto_subseq_of_limsup_edist_le in TauCeti/Topology/EMetricSpace/Ascoli.lean

LeanTauCeti.tendsto_subseq_of_limsup_edist_le

TheoremAlexandrov's theorem and its converse#

a subset of a completely metrizable space is completely metrizable in the subspace topology if and only if it is a Gδ set.

TauCeti.isGδ_iff_isCompletelyMetrizableSpace.{u_1} {X : Type u_1} [TopologicalSpace X]
  [TopologicalSpace.IsCompletelyMetrizableSpace X] {s : Set X} :
  IsGδ s ↔ TopologicalSpace.IsCompletelyMetrizableSpace ↑s

Lean

Formalized in Tau Ceti as TauCeti.isGδ_iff_isCompletelyMetrizableSpace.

Sources

• Tau Ceti documentation: TauCeti.isGδ_iff_isCompletelyMetrizableSpace
• Source of TauCeti.isGδ_iff_isCompletelyMetrizableSpace in TauCeti/Topology/MetricSpace/Polish/GDelta.lean

LeanTauCeti.isGδ_iff_isCompletelyMetrizableSpace

TheoremThe Arzelà–Ascoli theorem in C(X, Y)#

On a space X whose topology is coherent with its compact sets (for instance a locally compact space), an equicontinuous set of continuous maps whose values at each point lie in a common compact set has compact closure in the compact-open topology.

ArzelaAscoli.isCompact_closure_of_equicontinuous.{u_1, u_2} {X : Type u_1} {Y : Type u_2}
  [TopologicalSpace X] [CompactlyCoherentSpace X] [UniformSpace Y] {A : Set C(X, Y)}
  (hA : Equicontinuous fun f => ⇑↑f) (hApt : ∀ (x : X), ∃ Q, IsCompact Q ∧ ∀ f ∈ A, f x ∈ Q) :
  IsCompact (closure A)

Lean

Formalized in Tau Ceti as ArzelaAscoli.isCompact_closure_of_equicontinuous.

Other forms

The Arzelà–Ascoli theorem in C(X, Y), with a dense set of points. Formalized in Tau Ceti as ArzelaAscoli.isCompact_closure_of_equicontinuous_of_totallyBounded.

ArzelaAscoli.isCompact_closure_of_equicontinuous_of_totallyBounded.{u_1, u_2} {X : Type u_1}
  {Y : Type u_2} [TopologicalSpace X] [CompactlyCoherentSpace X] [UniformSpace Y] [CompleteSpace Y]
  {A : Set C(X, Y)} {D : Set X} (hD : Dense D) (hA : Equicontinuous fun f => ⇑↑f)
  (hAD : ∀ x ∈ D, TotallyBounded ((fun f => f x) '' A)) : IsCompact (closure A)

Sources

• Tau Ceti documentation: ArzelaAscoli.isCompact_closure_of_equicontinuous
• Source of ArzelaAscoli.isCompact_closure_of_equicontinuous in TauCeti/Topology/ContinuousMap/Ascoli.lean

LeanArzelaAscoli.isCompact_closure_of_equicontinuous · ArzelaAscoli.isCompact_closure_of_equicontinuous_of_totallyBounded

Used by 3

Used byMontel's theorem as an equivalence · The Fréchet--Kolmogorov compactness criterion · Lisini's superposition principle in a complete separable metric space

TheoremCartan's criterion#

Let B be a set of quasi-compact opens of X which is closed under binary intersections and contains, inside each of its members, a basis of the topology of that member. A sheaf of abelian groups which is Čech acyclic for the finite covers of members of B by members of B has no cohomology in positive degrees on the members of B.

TauCeti.Topology.subsingleton_H'_succ_of_isCechAcyclicOn.{u} {X : TopCat}
  {B : Set (TopologicalSpace.Opens ↑X)}
  {F : CategoryTheory.Sheaf (Opens.grothendieckTopology ↑X) AddCommGrpCat}
  (hinf : ∀ U ∈ B, ∀ V ∈ B, U ⊓ V ∈ B) (hcpt : ∀ U ∈ B, IsCompact ↑U)
  (hbasis : ∀ U ∈ B, ∀ V ≤ U, ∀ x ∈ V, ∃ W ∈ B, x ∈ W ∧ W ≤ V)
  (hF : TauCeti.Topology.IsCechAcyclicOn B F) {Y : TopologicalSpace.Opens ↑X} (hY : Y ∈ B) (n : ℕ) :
  Subsingleton ↑(F.H' (n + 1) Y)

Lean

Formalized in Tau Ceti as TauCeti.Topology.subsingleton_H'_succ_of_isCechAcyclicOn.

Sources

• Tau Ceti documentation: TauCeti.Topology.subsingleton_H'_succ_of_isCechAcyclicOn
• Source of TauCeti.Topology.subsingleton_H'_succ_of_isCechAcyclicOn in TauCeti/Topology/Sheaves/Cartan.lean

LeanTauCeti.Topology.subsingleton_H'_succ_of_isCechAcyclicOn

Used by 1

Used bySerre's vanishing theorem on affine opens

TheoremThe cellular approximation theorem (Hatcher, Theorem 4.8)#

Every map f : C → C' of relative CW complexes sending the base D into the base E is homotopic, relative to D, to a cellular map.

TauCeti.exists_isCellular_homotopicRel.{w} {X Y : Type w} [TopologicalSpace X] [T2Space X]
  [TopologicalSpace Y] [T2Space Y] {C D : Set X} [Topology.RelCWComplex C D] {C' E : Set Y}
  [Topology.RelCWComplex C' E] (f : ↧↑C ⟶ ↧↑C')
  (hf : Set.MapsTo ⇑(CategoryTheory.ConcreteCategory.hom f) {x | ↑x ∈ D} {y | ↑y ∈ E}) :
  ∃ g, TauCeti.IsCellular C C' g ∧ (TopCat.Hom.hom f).HomotopicRel (TopCat.Hom.hom g) {x | ↑x ∈ D}

Lean

Formalized in Tau Ceti as TauCeti.exists_isCellular_homotopicRel.

Other forms

The cellular approximation theorem for CW complexes (Hatcher, Theorem 4.8). Formalized in Tau Ceti as TauCeti.exists_isCellular_homotopic.

TauCeti.exists_isCellular_homotopic.{w} {X Y : Type w} [TopologicalSpace X] [T2Space X]
  [TopologicalSpace Y] [T2Space Y] {C : Set X} [Topology.CWComplex C] {C' : Set Y}
  [Topology.CWComplex C'] (f : ↧↑C ⟶ ↧↑C') :
  ∃ g, TauCeti.IsCellular C C' g ∧ (TopCat.Hom.hom f).Homotopic (TopCat.Hom.hom g)

Sources

• Tau Ceti documentation: TauCeti.exists_isCellular_homotopicRel
• Source of TauCeti.exists_isCellular_homotopicRel in TauCeti/Topology/CWComplex/Classical/CellularApproximation.lean

LeanTauCeti.exists_isCellular_homotopicRel · TauCeti.exists_isCellular_homotopic

TheoremEkeland's variational principle#

Let φ be a lower semicontinuous function, bounded below, on a complete metric space, and let ε > 0. For every x there is a point y such that φ y + ε * dist y x ≤ φ x and y is the strict global minimum of z ↦ φ z + ε * dist z y.

LowerSemicontinuous.exists_add_mul_dist_le_and_lt_add_mul_dist.{u_1} {X : Type u_1} [MetricSpace X]
  [CompleteSpace X] {φ : X → ℝ} (hφ : LowerSemicontinuous φ) (hbdd : BddBelow (Set.range φ)) {ε : ℝ}
  (hε : 0 < ε) (x : X) : ∃ y, φ y + ε * dist y x ≤ φ x ∧ ∀ (z : X), z ≠ y → φ y < φ z + ε * dist z y

Lean

Formalized in Tau Ceti as LowerSemicontinuous.exists_add_mul_dist_le_and_lt_add_mul_dist.

Sources

• Tau Ceti documentation: LowerSemicontinuous.exists_add_mul_dist_le_and_lt_add_mul_dist
• Source of LowerSemicontinuous.exists_add_mul_dist_le_and_lt_add_mul_dist in TauCeti/Topology/MetricSpace/Ekeland.lean

LeanLowerSemicontinuous.exists_add_mul_dist_le_and_lt_add_mul_dist

Used by 1

Used byBishop–Phelps support lemma

TheoremGrothendieck's inequality#

Grothendieck's inequality for bounded real bilinear forms on spaces of continuous functions, with constant κ_ℝ = 8. Let K and L be compact normal spaces and B a bilinear form on C(K, ℝ) × C(L, ℝ) with |B f g| ≤ C * ‖f‖ * ‖g‖. If ∑ i, f i x ^ 2 ≤ 1 and ∑ i, g i y ^ 2 ≤ 1 everywhere, then |∑ i, B (f i) (g i)| ≤ 8 * C.

LinearMap.abs_sum_apply_apply_le_eight_mul.{u_1, u_2, u_4} {K : Type u_1} {L : Type u_2}
  {ι : Type u_4} [TopologicalSpace K] [CompactSpace K] [TopologicalSpace L] [CompactSpace L]
  [Fintype ι] [NormalSpace K] [NormalSpace L] (B : C(K, ℝ) →ₗ[ℝ] C(L, ℝ) →ₗ[ℝ] ℝ) {C : ℝ}
  (hC : 0 ≤ C) (hB : ∀ (f : C(K, ℝ)) (g : C(L, ℝ)), |(B f) g| ≤ C * ‖f‖ * ‖g‖) {f : ι → C(K, ℝ)}
  {g : ι → C(L, ℝ)} (hf : ∀ (x : K), ∑ i, (f i) x ^ 2 ≤ 1) (hg : ∀ (y : L), ∑ i, (g i) y ^ 2 ≤ 1) :
  |∑ i, (B (f i)) (g i)| ≤ 8 * C

Lean

Formalized in Tau Ceti as LinearMap.abs_sum_apply_apply_le_eight_mul.

Other forms

Grothendieck's inequality. Formalized in Tau Ceti as LinearMap.norm_sum_apply_apply_le_sixteen_mul.

LinearMap.norm_sum_apply_apply_le_sixteen_mul.{u_1, u_2, u_3, u_4} {K : Type u_1} {L : Type u_2}
  {𝕜 : Type u_3} {ι : Type u_4} [TopologicalSpace K] [CompactSpace K] [TopologicalSpace L]
  [CompactSpace L] [RCLike 𝕜] [Fintype ι] [NormalSpace K] [NormalSpace L]
  (B : C(K, 𝕜) →ₗ[𝕜] C(L, 𝕜) →ₗ[𝕜] 𝕜) {C : ℝ} (hC : 0 ≤ C)
  (hB : ∀ (f : C(K, 𝕜)) (g : C(L, 𝕜)), ‖(B f) g‖ ≤ C * ‖f‖ * ‖g‖) {f : ι → C(K, 𝕜)}
  {g : ι → C(L, 𝕜)} (hf : ∀ (x : K), ∑ i, ‖(f i) x‖ ^ 2 ≤ 1)
  (hg : ∀ (y : L), ∑ i, ‖(g i) y‖ ^ 2 ≤ 1) : ‖∑ i, (B (f i)) (g i)‖ ≤ 16 * C

Sources

• Tau Ceti documentation: LinearMap.abs_sum_apply_apply_le_eight_mul
• Source of LinearMap.abs_sum_apply_apply_le_eight_mul in TauCeti/Topology/ContinuousMap/Grothendieck.lean

LeanLinearMap.abs_sum_apply_apply_le_eight_mul · LinearMap.norm_sum_apply_apply_le_sixteen_mul

Uses 1

Proof usesGrothendieck's inequality over the reals, with constant κ_ℝ = 8

DefinitionLeray's theorem#

Let U be a finite family of opens covering a topological space X, and let F be a sheaf of abelian groups on X with no cohomology in positive degrees on any nonempty finite intersection of members of U. Then the Čech cohomology Hⁿ(U, F), the cohomology of the Čech complex of F for U, is isomorphic to the sheaf cohomology Hⁿ(X, F), for every n, naturally in F (TauCeti.Topology.homologyMap_comp_homologyCechComplexIsoH_hom).

TauCeti.Topology.homologyCechComplexIsoH.{u} {X : TopCat} {ι : Type u}
  (U : ι → TopologicalSpace.Opens ↑X) (hU : ⨆ i, U i = ⊤) [Finite ι]
  (F : CategoryTheory.Sheaf (Opens.grothendieckTopology ↑X) AddCommGrpCat)
  (hF : ∀ (s : Finset ι), s.Nonempty → ∀ (k : ℕ), Subsingleton ↑(F.H' (k + 1) (s.inf U))) (n : ℕ) :
  HomologicalComplex.homology ((CategoryTheory.cechComplexFunctor U).obj F.obj) n ≅ ↧(F.H n)

Lean

Formalized in Tau Ceti as TauCeti.Topology.homologyCechComplexIsoH.

Sources

• Tau Ceti documentation: TauCeti.Topology.homologyCechComplexIsoH
• Source of TauCeti.Topology.homologyCechComplexIsoH in TauCeti/Topology/Sheaves/Leray.lean

LeanTauCeti.Topology.homologyCechComplexIsoH

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.