LeftRight

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

Statistics

Metric	Count
Definitions	0
Theorems `exists_gt`, `exists_lt`, `interior_eq_empty`, `interior_eq_empty'`, `continuousAt_iff_continuous_left'_right'`, `continuousAt_iff_continuous_left_right`, `continuousWithinAt_Iio_iff_Iic`, `continuousWithinAt_Ioi_iff_Ici`, `continuousWithinAt_iff_continuous_left'_right'`, `continuousWithinAt_iff_continuous_left_right`, `continuousWithinAt_inter_Iio_iff_Iic`, `continuousWithinAt_inter_Ioi_iff_Ici`, `frequently_gt_nhds`, `frequently_lt_nhds`, `nhdsGE_neBot`, `nhdsGT_le_nhdsNE`, `nhdsGT_sup_nhdsWithin_singleton`, `nhdsLE_neBot`, `nhdsLE_sup_nhdsGE`, `nhdsLE_sup_nhdsGT`, `nhdsLT_le_nhdsNE`, `nhdsLT_sup_nhdsGE`, `nhdsLT_sup_nhdsGT`, `nhdsWithinLE_sup_nhdsWithinGE`, `nhdsWithinLE_sup_nhdsWithinGT`, `nhdsWithinLT_sup_nhdsWithinGE`, `nhdsWithinLT_sup_nhdsWithinGT`, `nhdsWithin_Ici_neBot`, `nhdsWithin_Iic_neBot`, `nhdsWithin_uIoo_left_le_nhdsNE`, `nhdsWithin_uIoo_right_le_nhdsNE`	31
Total	31

Filter.Eventually

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_gt` 📖	mathematical	`Filter.Eventually` `nhds`	`Preorder.toLT`	—	`Filter.Frequently.exists` `Filter.Frequently.and_eventually` `frequently_gt_nhds`
`exists_lt` 📖	mathematical	`Filter.Eventually` `nhds`	`Preorder.toLT`	—	`Filter.Frequently.exists` `Filter.Frequently.and_eventually` `frequently_lt_nhds`

IsAntichain

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`interior_eq_empty` 📖	mathematical	`Filter.NeBot` `nhdsWithin` `Set.Iio` `IsAntichain` `Preorder.toLE`	`interior` `Set` `Set.instEmptyCollection`	—	`Set.eq_empty_of_forall_notMem` `mem_interior_iff_mem_nhds` `Filter.Eventually.exists_lt` `interior_subset` `LT.lt.ne` `LT.lt.le`
`interior_eq_empty'` 📖	mathematical	`Filter.NeBot` `nhdsWithin` `Set.Ioi` `IsAntichain` `Preorder.toLE`	`interior` `Set` `Set.instEmptyCollection`	—	`interior_eq_empty` `to_dual`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuousAt_iff_continuous_left'_right'` 📖	mathematical	—	`ContinuousAt` `ContinuousWithinAt` `Set.Iio` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.Ioi`	—	`continuousWithinAt_Ioi_iff_Ici` `continuousWithinAt_Iio_iff_Iic` `continuousAt_iff_continuous_left_right`
`continuousAt_iff_continuous_left_right` 📖	mathematical	—	`ContinuousAt` `ContinuousWithinAt` `Set.Iic` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.Ici`	—	`nhdsLE_sup_nhdsGE`
`continuousWithinAt_Iio_iff_Iic` 📖	mathematical	—	`ContinuousWithinAt` `Set.Iio` `PartialOrder.toPreorder` `Set.Iic`	—	`continuousWithinAt_Ioi_iff_Ici`
`continuousWithinAt_Ioi_iff_Ici` 📖	mathematical	—	`ContinuousWithinAt` `Set.Ioi` `PartialOrder.toPreorder` `Set.Ici`	—	—
`continuousWithinAt_iff_continuous_left'_right'` 📖	mathematical	—	`ContinuousWithinAt` `Set` `Set.instInter` `Set.Iio` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.Ioi`	—	`continuousWithinAt_inter_Ioi_iff_Ici` `continuousWithinAt_inter_Iio_iff_Iic` `continuousWithinAt_iff_continuous_left_right`
`continuousWithinAt_iff_continuous_left_right` 📖	mathematical	—	`ContinuousWithinAt` `Set` `Set.instInter` `Set.Iic` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.Ici`	—	`nhdsWithinLE_sup_nhdsWithinGE`
`continuousWithinAt_inter_Iio_iff_Iic` 📖	mathematical	—	`ContinuousWithinAt` `Set` `Set.instInter` `Set.Iio` `PartialOrder.toPreorder` `Set.Iic`	—	`continuousWithinAt_inter_Ioi_iff_Ici`
`continuousWithinAt_inter_Ioi_iff_Ici` 📖	mathematical	—	`ContinuousWithinAt` `Set` `Set.instInter` `Set.Ioi` `PartialOrder.toPreorder` `Set.Ici`	—	—
`frequently_gt_nhds` 📖	mathematical	—	`Filter.Frequently` `Preorder.toLT` `nhds`	—	`Filter.frequently_iff_neBot`
`frequently_lt_nhds` 📖	mathematical	—	`Filter.Frequently` `Preorder.toLT` `nhds`	—	`Filter.frequently_iff_neBot`
`nhdsGE_neBot` 📖	mathematical	—	`Filter.NeBot` `nhdsWithin` `Set.Ici`	—	`nhdsWithin_Ici_neBot` `le_refl`
`nhdsGT_le_nhdsNE` 📖	mathematical	—	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `nhdsWithin` `Set.Ioi` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet`	—	`nhdsWithin_mono` `ne_of_gt`
`nhdsGT_sup_nhdsWithin_singleton` 📖	mathematical	—	`Filter` `Filter.instSup` `nhdsWithin` `Set.Ioi` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set` `Set.instSingletonSet` `Set.Ici`	—	`Set.union_singleton` `Set.Ioi_insert`
`nhdsLE_neBot` 📖	mathematical	—	`Filter.NeBot` `nhdsWithin` `Set.Iic`	—	`nhdsWithin_Iic_neBot` `le_refl`
`nhdsLE_sup_nhdsGE` 📖	mathematical	—	`Filter` `Filter.instSup` `nhdsWithin` `Set.Iic` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.Ici` `nhds`	—	`nhdsWithin_union` `Set.Iic_union_Ici` `nhdsWithin_univ`
`nhdsLE_sup_nhdsGT` 📖	mathematical	—	`Filter` `Filter.instSup` `nhdsWithin` `Set.Iic` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.Ioi` `nhds`	—	`nhdsWithin_union` `Set.Iic_union_Ioi` `nhdsWithin_univ`
`nhdsLT_le_nhdsNE` 📖	mathematical	—	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `nhdsWithin` `Set.Iio` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet`	—	`nhdsWithin_mono` `ne_of_lt`
`nhdsLT_sup_nhdsGE` 📖	mathematical	—	`Filter` `Filter.instSup` `nhdsWithin` `Set.Iio` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.Ici` `nhds`	—	`nhdsWithin_union` `Set.Iio_union_Ici` `nhdsWithin_univ`
`nhdsLT_sup_nhdsGT` 📖	mathematical	—	`Filter` `Filter.instSup` `nhdsWithin` `Set.Iio` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.Ioi` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet`	—	`nhdsWithin_union` `Set.Iio_union_Ioi`
`nhdsWithinLE_sup_nhdsWithinGE` 📖	mathematical	—	`Filter` `Filter.instSup` `nhdsWithin` `Set` `Set.instInter` `Set.Iic` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.Ici`	—	`nhdsWithin_union` `Set.inter_union_distrib_left` `Set.Iic_union_Ici` `Set.inter_univ`
`nhdsWithinLE_sup_nhdsWithinGT` 📖	mathematical	—	`Filter` `Filter.instSup` `nhdsWithin` `Set` `Set.instInter` `Set.Iic` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.Ioi`	—	`nhdsWithin_union` `Set.inter_union_distrib_left` `Set.Iic_union_Ioi` `Set.inter_univ`
`nhdsWithinLT_sup_nhdsWithinGE` 📖	mathematical	—	`Filter` `Filter.instSup` `nhdsWithin` `Set` `Set.instInter` `Set.Iio` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.Ici`	—	`nhdsWithin_union` `Set.inter_union_distrib_left` `Set.Iio_union_Ici` `Set.inter_univ`
`nhdsWithinLT_sup_nhdsWithinGT` 📖	mathematical	—	`Filter` `Filter.instSup` `nhdsWithin` `Set` `Set.instInter` `Set.Iio` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.Ioi` `Set.instSDiff` `Set.instSingletonSet`	—	`nhdsWithin_union` `Set.inter_union_distrib_left` `Set.Iio_union_Ioi` `Set.compl_eq_univ_diff` `Set.inter_sdiff_left_comm` `Set.univ_inter`
`nhdsWithin_Ici_neBot` 📖	mathematical	`Preorder.toLE`	`Filter.NeBot` `nhdsWithin` `Set.Ici`	—	`nhdsWithin_neBot_of_mem`
`nhdsWithin_Iic_neBot` 📖	mathematical	`Preorder.toLE`	`Filter.NeBot` `nhdsWithin` `Set.Iic`	—	`nhdsWithin_neBot_of_mem`
`nhdsWithin_uIoo_left_le_nhdsNE` 📖	mathematical	—	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `nhdsWithin` `Set.uIoo` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet`	—	`nhdsWithin_mono`
`nhdsWithin_uIoo_right_le_nhdsNE` 📖	mathematical	—	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `nhdsWithin` `Set.uIoo` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet`	—	`nhdsWithin_mono`

---

← Back to Index