CountableSeparating

📁 Source: Mathlib/Topology/Order/CountableSeparating.lean

Statistics

Metric	Count
Definitions	0
Theorems of_forall_eventually_ge_iff, of_forall_eventually_gt_iff, of_forall_eventually_le_iff, of_forall_eventually_lt_iff, range_Ici, range_Iic, range_Iio, range_Ioi	8
Total	8

Filter.EventuallyEq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_forall_eventually_ge_iff 📖	mathematical	Filter.Eventually Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Filter.EventuallyEq	—	of_forall_eventually_le_iff instOrderTopologyOrderDual instSecondCountableTopologyOrderDual
of_forall_eventually_gt_iff 📖	mathematical	Filter.Eventually Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Filter.EventuallyEq	—	of_forall_eventually_lt_iff instOrderTopologyOrderDual instSecondCountableTopologyOrderDual
of_forall_eventually_le_iff 📖	mathematical	Filter.Eventually Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Filter.EventuallyEq	—	of_forall_separating_preimage HasCountableSeparatingOn.range_Iic Set.forall_mem_range Filter.Eventually.set_eq
of_forall_eventually_lt_iff 📖	mathematical	Filter.Eventually Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Filter.EventuallyEq	—	of_forall_separating_preimage HasCountableSeparatingOn.range_Iio Set.forall_mem_range Filter.Eventually.set_eq

HasCountableSeparatingOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
range_Ici 📖	mathematical	—	HasCountableSeparatingOn Set Set.instMembership Set.range Set.Ici PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	range_Iic instOrderTopologyOrderDual instSecondCountableTopologyOrderDual
range_Iic 📖	mathematical	—	HasCountableSeparatingOn Set Set.instMembership Set.range Set.Iic PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	exists_countable_separating range_Ioi Set.Countable.image compl_inj_iff Set.compl_Ioi
range_Iio 📖	mathematical	—	HasCountableSeparatingOn Set Set.instMembership Set.range Set.Iio PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	TopologicalSpace.exists_countable_dense TopologicalSpace.SecondCountableTopology.to_separableSpace Set.Countable.image Set.Countable.union countable_setOf_covBy_left Set.image_subset_range Set.eq_empty_or_nonempty LT.lt.not_ge Set.mem_image_of_mem Set.ext_iff Dense.inter_open_nonempty isOpen_Ioo OrderTopology.to_orderClosedTopology LT.lt.not_gt Ne.lt_or_gt
range_Ioi 📖	mathematical	—	HasCountableSeparatingOn Set Set.instMembership Set.range Set.Ioi PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	range_Iio instOrderTopologyOrderDual instSecondCountableTopologyOrderDual

---

← Back to Index