SuccPred

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

Statistics

Metric	Count
Definitions	0
Theorems isOpen_iff, isOpen_singleton_iff, isOpen_singleton_of_not_isPredPrelimit, isPredLimit_of_mem_frontier, nhds_eq_pure, isOpen_iff, isOpen_singleton_iff, isOpen_singleton_of_not_isSuccPrelimit, isSuccLimit_of_mem_frontier, nhds_eq_pure	10
Total	10

PredOrder

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isOpen_iff 📖	mathematical	—	IsOpen Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set Set.instHasSubset Set.Ioo	—	isOpen_iff_mem_nhds Filter.HasBasis.mem_iff hasBasis_nhds_Ioc_of_exists_gt not_isMax_iff Order.IsPredLimit.not_isMax nhds_eq_pure instIsEmptyFalse
isOpen_singleton_iff 📖	mathematical	—	IsOpen Set Set.instSingletonSet Order.IsPredLimit PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	SuccOrder.isOpen_singleton_iff instOrderTopologyOrderDual OrderDual.noMaxOrder Iff.not Order.isSuccLimit_toDual_iff
isOpen_singleton_of_not_isPredPrelimit 📖	mathematical	Order.IsPredPrelimit Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	IsOpen Set Set.instSingletonSet	—	SuccOrder.isOpen_singleton_of_not_isSuccPrelimit instOrderTopologyOrderDual Iff.not Order.isSuccPrelimit_toDual_iff
isPredLimit_of_mem_frontier 📖	mathematical	Set Set.instMembership frontier	Order.IsPredLimit PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	Order.isSuccLimit_toDual_iff SuccOrder.isSuccLimit_of_mem_frontier instOrderTopologyOrderDual OrderDual.noMaxOrder
nhds_eq_pure 📖	mathematical	—	nhds Filter Filter.instPure Order.IsPredLimit PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	isOpen_singleton_iff_nhds_eq_pure isOpen_singleton_iff

SuccOrder

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isOpen_iff 📖	mathematical	—	IsOpen Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set Set.instHasSubset Set.Ioo	—	isOpen_iff_mem_nhds Filter.HasBasis.mem_iff hasBasis_nhds_Ioc_of_exists_lt not_isMin_iff Order.IsSuccLimit.not_isMin nhds_eq_pure instIsEmptyFalse
isOpen_singleton_iff 📖	mathematical	—	IsOpen Set Set.instSingletonSet Order.IsSuccLimit PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim Finite.instDiscreteTopology T2Space.t1Space OrderClosedTopology.to_t2Space OrderTopology.to_orderClosedTopology Finite.of_subsingleton WellFoundedGT.toIsSuccArchimedean IsWellOrder.toIsWellFounded isWellOrder_gt Finite.to_wellFoundedGT mem_nhds_iff_exists_Ioo_subset' Order.IsSuccLimit.not_isMin not_isMax IsOpen.mem_nhds Set.mem_singleton Order.IsSuccLimit.isSuccPrelimit Order.succ_eq_iff_covBy Order.lt_succ LE.le.trans_lt LT.lt.succ_le Order.not_isSuccLimit_iff Order.Iio_succ IsMin.Iic_eq isOpen_Iio instClosedIciTopology isOpen_singleton_of_not_isSuccPrelimit
isOpen_singleton_of_not_isSuccPrelimit 📖	mathematical	Order.IsSuccPrelimit Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	IsOpen Set Set.instSingletonSet	—	Order.not_isSuccPrelimit_iff_exists_covBy CovBy.Ioi_eq isOpen_Ioi instClosedIicTopology OrderTopology.to_orderClosedTopology CovBy.Ioo_eq_Ioc Order.covBy_succ_of_not_isMax CovBy.Ioc_eq isOpen_Ioo
isSuccLimit_of_mem_frontier 📖	mathematical	Set Set.instMembership frontier	Order.IsSuccLimit PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	Iff.not_left isOpen_singleton_iff frontier_eq_closure_inter_closure
nhds_eq_pure 📖	mathematical	—	nhds Filter Filter.instPure Order.IsSuccLimit PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	isOpen_singleton_iff_nhds_eq_pure isOpen_singleton_iff

---

← Back to Index