AtTopBotIxx

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

Statistics

Metric	Count
Definitions	0
Theorems comap_coe_Iio_nhdsLT, comap_coe_Ioi_nhdsGT, comap_coe_Ioo_nhdsGT, comap_coe_Ioo_nhdsLT, comap_coe_nhdsGT_eq_atBot_iff, comap_coe_nhdsGT_of_Ioo_subset, comap_coe_nhdsLT_eq_atTop_iff, comap_coe_nhdsLT_of_Ioo_subset, map_coe_Iio_atTop, map_coe_Ioi_atBot, map_coe_Ioo_atBot, map_coe_Ioo_atTop, map_coe_atBot_of_Ioo_subset, map_coe_atTop_of_Ioo_subset, tendsto_Iio_atTop, tendsto_Ioi_atBot, tendsto_Ioo_atBot, tendsto_Ioo_atTop, tendsto_comp_coe_Iio_atTop, tendsto_comp_coe_Ioi_atBot, tendsto_comp_coe_Ioo_atBot, tendsto_comp_coe_Ioo_atTop	22
Total	22

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comap_coe_Iio_nhdsLT 📖	mathematical	Order.IsSuccPrelimit Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Filter.comap Set Set.instMembership Set.Iio nhdsWithin Filter.atTop Subtype.preorder	—	comap_coe_Ioi_nhdsGT instOrderTopologyOrderDual Order.IsSuccPrelimit.dual
comap_coe_Ioi_nhdsGT 📖	mathematical	Order.IsPredPrelimit Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Filter.comap Set Set.instMembership Set.Ioi nhdsWithin Filter.atBot Subtype.preorder	—	comap_coe_nhdsGT_of_Ioo_subset Set.Subset.rfl Set.Ioo_subset_Ioi_self
comap_coe_Ioo_nhdsGT 📖	mathematical	Order.IsPredPrelimit Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Filter.comap Set Set.instMembership Set.Ioo nhdsWithin Set.Ioi Filter.atBot Subtype.preorder	—	comap_coe_nhdsGT_of_Ioo_subset Set.Ioo_subset_Ioi_self LT.lt.trans Set.Subset.rfl
comap_coe_Ioo_nhdsLT 📖	mathematical	Order.IsSuccPrelimit Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Filter.comap Set Set.instMembership Set.Ioo nhdsWithin Set.Iio Filter.atTop Subtype.preorder	—	comap_coe_nhdsLT_of_Ioo_subset Set.Ioo_subset_Iio_self LT.lt.trans Set.Subset.rfl
comap_coe_nhdsGT_eq_atBot_iff 📖	mathematical	—	Filter.comap Set Set.instMembership nhdsWithin Set.Ioi PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Filter.atBot Subtype.preorder Set.instHasSubset Set.Nonempty Set.instInter Set.Ioo	—	comap_coe_nhdsLT_eq_atTop_iff instOrderTopologyOrderDual EquivLike.range_eq_univ Equiv.surjective Set.Ioo_toDual
comap_coe_nhdsGT_of_Ioo_subset 📖	mathematical	Set Set.instHasSubset Set.Ioi PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLT Set.Ioo Order.IsPredPrelimit	Filter.comap Set.instMembership nhdsWithin Filter.atBot Subtype.preorder	—	comap_coe_nhdsLT_of_Ioo_subset instOrderTopologyOrderDual Set.Ioo_toDual Order.IsPredPrelimit.dual
comap_coe_nhdsLT_eq_atTop_iff 📖	mathematical	—	Filter.comap Set Set.instMembership nhdsWithin Set.Iio PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Filter.atTop Subtype.preorder Set.instHasSubset Set.Nonempty Set.instInter Set.Ioo	—	Set.eq_empty_or_nonempty Unique.instSubsingleton Set.instIsEmptyElemEmptyCollection Set.empty_inter instIsEmptyFalse Set.Nonempty.to_subtype Filter.preimage_mem_comap Ioo_mem_nhdsLT instClosedIicTopology OrderTopology.to_orderClosedTopology Filter.nonempty_of_mem Filter.atTop_neBot SemilatticeSup.instIsDirectedOrder Filter.HasBasis.ext Filter.HasBasis.comap nhdsLT_basis_of_exists_lt Set.Nonempty.mono Filter.atTop_basis LT.lt.trans_le Set.not_subset_iff_exists_mem_notMem Filter.Eventually.exists Filter.Eventually.and Filter.Tendsto.eventually eventually_mem_nhdsWithin Filter.eventually_ge_atTop lt_irrefl Mathlib.Tactic.Contrapose.contrapose₂
comap_coe_nhdsLT_of_Ioo_subset 📖	mathematical	Set Set.instHasSubset Set.Iio PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLT Set.Ioo Order.IsSuccPrelimit	Filter.comap Set.instMembership nhdsWithin Filter.atTop Subtype.preorder	—	comap_coe_nhdsLT_eq_atTop_iff Order.IsSuccPrelimit.lt_iff_exists_lt max_lt max_lt_iff
map_coe_Iio_atTop 📖	mathematical	Order.IsSuccPrelimit Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Filter.map Set Set.instMembership Set.Iio Filter.atTop Subtype.preorder nhdsWithin	—	map_coe_Ioi_atBot instOrderTopologyOrderDual Order.IsSuccPrelimit.dual
map_coe_Ioi_atBot 📖	mathematical	Order.IsPredPrelimit Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Filter.map Set Set.instMembership Set.Ioi Filter.atBot Subtype.preorder nhdsWithin	—	map_coe_atBot_of_Ioo_subset Set.Subset.rfl Set.Ioo_subset_Ioi_self
map_coe_Ioo_atBot 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Order.IsPredPrelimit	Filter.map Set Set.instMembership Set.Ioo Filter.atBot Subtype.preorder nhdsWithin Set.Ioi	—	map_coe_atBot_of_Ioo_subset Set.Ioo_subset_Ioi_self Set.Subset.rfl
map_coe_Ioo_atTop 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Order.IsSuccPrelimit	Filter.map Set Set.instMembership Set.Ioo Filter.atTop Subtype.preorder nhdsWithin Set.Iio	—	map_coe_atTop_of_Ioo_subset Set.Ioo_subset_Iio_self Set.Subset.rfl
map_coe_atBot_of_Ioo_subset 📖	mathematical	Set Set.instHasSubset Set.Ioi PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLT Set.Ioo Order.IsPredPrelimit	Filter.map Set.instMembership Filter.atBot Subtype.preorder nhdsWithin	—	map_coe_atTop_of_Ioo_subset instOrderTopologyOrderDual Set.Ioo_toDual EquivLike.range_eq_univ Order.IsPredPrelimit.dual
map_coe_atTop_of_Ioo_subset 📖	mathematical	Set Set.instHasSubset Set.Iio PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLT Set.Ioo Order.IsSuccPrelimit	Filter.map Set.instMembership Filter.atTop Subtype.preorder nhdsWithin	—	Set.eq_empty_or_nonempty Eq.subset Set.instReflSubset Filter.filter_eq_bot_of_isEmpty Filter.map_bot nhdsWithin_empty comap_coe_nhdsLT_of_Ioo_subset Filter.map_comap_of_mem Subtype.range_val mem_nhdsLT_iff_exists_Ioo_subset'
tendsto_Iio_atTop 📖	mathematical	Order.IsSuccPrelimit Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Filter.Tendsto Set.Elem Set.Iio Filter.atTop Subtype.preorder Set Set.instMembership nhdsWithin	—	comap_coe_Iio_nhdsLT Filter.tendsto_comap_iff
tendsto_Ioi_atBot 📖	mathematical	Order.IsPredPrelimit Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Filter.Tendsto Set.Elem Set.Ioi Filter.atBot Subtype.preorder Set Set.instMembership nhdsWithin	—	comap_coe_Ioi_nhdsGT Filter.tendsto_comap_iff
tendsto_Ioo_atBot 📖	mathematical	Order.IsPredPrelimit Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Filter.Tendsto Set.Elem Set.Ioo Filter.atBot Subtype.preorder Set Set.instMembership nhdsWithin Set.Ioi	—	comap_coe_Ioo_nhdsGT Filter.tendsto_comap_iff
tendsto_Ioo_atTop 📖	mathematical	Order.IsSuccPrelimit Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Filter.Tendsto Set.Elem Set.Ioo Filter.atTop Subtype.preorder Set Set.instMembership nhdsWithin Set.Iio	—	comap_coe_Ioo_nhdsLT Filter.tendsto_comap_iff
tendsto_comp_coe_Iio_atTop 📖	mathematical	Order.IsSuccPrelimit Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Filter.Tendsto Set.Elem Set.Iio Set Set.instMembership Filter.atTop Subtype.preorder nhdsWithin	—	map_coe_Iio_atTop Filter.tendsto_map'_iff
tendsto_comp_coe_Ioi_atBot 📖	mathematical	Order.IsPredPrelimit Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Filter.Tendsto Set.Elem Set.Ioi Set Set.instMembership Filter.atBot Subtype.preorder nhdsWithin	—	map_coe_Ioi_atBot Filter.tendsto_map'_iff
tendsto_comp_coe_Ioo_atBot 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Order.IsPredPrelimit	Filter.Tendsto Set.Elem Set.Ioo Set Set.instMembership Filter.atBot Subtype.preorder nhdsWithin Set.Ioi	—	map_coe_Ioo_atBot Filter.tendsto_map'_iff
tendsto_comp_coe_Ioo_atTop 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Order.IsSuccPrelimit	Filter.Tendsto Set.Elem Set.Ioo Set Set.instMembership Filter.atTop Subtype.preorder nhdsWithin Set.Iio	—	map_coe_Ioo_atTop Filter.tendsto_map'_iff

---

← Back to Index