NotNormal

📁 Source: Mathlib/Topology/Separation/NotNormal.lean

Statistics

Metric	Count
Definitions	0
Theorems mk_lt_continuum, mk_lt_two_pow_mk_dense, not_normal_of_continuum_le_mk, two_pow_mk_le_two_pow_mk_dense, two_pow_mk_lt_continuum	5
Total	5

IsClosed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mk_lt_continuum 📖	mathematical	—	Cardinal Preorder.toLT PartialOrder.toPreorder Cardinal.partialOrder Set.Elem Cardinal.continuum	—	LT.lt.trans_le Nat.instAtLeastTwoHAddOfNat Cardinal.cantor two_pow_mk_lt_continuum
mk_lt_two_pow_mk_dense 📖	mathematical	Dense	Cardinal Preorder.toLT PartialOrder.toPreorder Cardinal.partialOrder Set.Elem Cardinal.instPowCardinal instOfNatAtLeastTwo Cardinal.instNatCast Nat.instAtLeastTwoHAddOfNat	—	LT.lt.trans_le Nat.instAtLeastTwoHAddOfNat Cardinal.cantor two_pow_mk_le_two_pow_mk_dense
not_normal_of_continuum_le_mk 📖	mathematical	—	NormalSpace	—	LT.lt.not_ge mk_lt_continuum
two_pow_mk_le_two_pow_mk_dense 📖	mathematical	Dense	Cardinal Cardinal.instLE Cardinal.instPowCardinal instOfNatAtLeastTwo Cardinal.instNatCast Nat.instAtLeastTwoHAddOfNat Set.Elem	—	Set.inter_eq_self_of_subset_right Subtype.image_preimage_val isClosedMap_subtype_val isClosed_discrete Dense.inter_open_nonempty IsOpen.inter Set.Nonempty.mono Set.subset_inter HasSubset.Subset.trans Set.instIsTransSubset Set.diff_subset Set.diff_subset_diff_left Set.diff_nonempty Set.Nonempty.not_disjoint Set.inter_right_comm Set.disjoint_of_subset_left Set.inter_subset_left SetCoe.ext HasSubset.Subset.antisymm Set.instAntisymmSubset Nat.instAtLeastTwoHAddOfNat Cardinal.mk_powerset Cardinal.mk_range_eq Cardinal.mk_le_mk_of_subset Set.range_subset_iff Set.inter_subset_right normal_separation Set.disjoint_sdiff_right
two_pow_mk_lt_continuum 📖	mathematical	—	Cardinal Cardinal.instLE Cardinal.instPowCardinal instOfNatAtLeastTwo Cardinal.instNatCast Nat.instAtLeastTwoHAddOfNat Set.Elem Cardinal.continuum	—	Nat.instAtLeastTwoHAddOfNat TopologicalSpace.exists_countable_dense two_pow_mk_le_two_pow_mk_dense Cardinal.power_le_power_left two_ne_zero ZeroLEOneClass.neZero.two IsOrderedRing.toZeroLEOneClass Cardinal.isOrderedRing NeZero.charZero_one Cardinal.instCharZero Cardinal.addLeftMono Set.Countable.le_aleph0 Cardinal.two_power_aleph0

---

← Back to Index