Mathlib Map

Theorems · Theorem · general topology

Set.Countable.isLindelof_sUnion

∀ {X : Type u} [inst : TopologicalSpace X] {S : Set (Set X)}, S.Countable → (∀ s ∈ S, IsLindelof s) → IsLindelof (⋃₀ S)
Defined in
Mathlib.Topology.Compactness.Lindelof
Cited by
1 results in Mathlib
Foundations
Depth 88 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
TopologicalSpace
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

isLindelof_iUnion · cited by 2isLindelof_iUnionSet · cited by 53352SetTopologicalSpace · cited by 24529TopologicalSpaceSet.Countable · cited by 545Set.CountableSet.sUnion · cited by 392Set.sUnionIsLindelof · cited by 85IsLindelofSet.sUnion_eq_biUnion · cited by 51Set.sUnion_eq_biUnionSet.Countable.isLindelof_biUnion · cited by 4Countable.isLindelof_biUn…Countable.isLindelof_sUnionCITED BYCITES

Cites7

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by1

Results whose statement or proof uses this declaration.