ExtendFrom

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

Statistics

Metric	Count
Definitions	0
Theorems continuousOn_Icc_extendFrom_Ioo, continuousOn_Ico_extendFrom_Ioo, continuousOn_Ioc_extendFrom_Ioo, continuousOn_uIcc_extendFrom_uIoo, eq_lim_at_left_extendFrom_Ioo, eq_lim_at_left_extendFrom_uIoo, eq_lim_at_right_extendFrom_Ioo, eq_lim_at_right_extendFrom_uIoo	8
Total	8

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuousOn_Icc_extendFrom_Ioo 📖	mathematical	ContinuousOn Set.Ioo PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Filter.Tendsto nhdsWithin Set.Ioi nhds Set.Iio	extendFrom Set.Icc	—	continuousOn_extendFrom closure_Ioo subset_refl Set.instReflSubset Set.eq_endpoints_or_mem_Ioo_of_mem_Icc Filter.Tendsto.mono_left nhdsWithin_mono Set.Ioo_subset_Ioi_self Set.Ioo_subset_Iio_self
continuousOn_Ico_extendFrom_Ioo 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder ContinuousOn Set.Ioo Filter.Tendsto nhdsWithin Set.Ioi nhds	extendFrom Set.Ico	—	continuousOn_extendFrom closure_Ioo LT.lt.ne Set.Ico_subset_Icc_self Set.eq_left_or_mem_Ioo_of_mem_Ico nhdsWithin_Ioo_eq_nhdsGT instClosedIciTopology OrderTopology.to_orderClosedTopology
continuousOn_Ioc_extendFrom_Ioo 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder ContinuousOn Set.Ioo Filter.Tendsto nhdsWithin Set.Iio nhds	extendFrom Set.Ioc	—	continuousOn_Ico_extendFrom_Ioo OrderDual.denselyOrdered instOrderTopologyOrderDual LT.lt.dual Set.Ioo_toDual Set.Ioi_toDual Set.Ico_toDual
continuousOn_uIcc_extendFrom_uIoo 📖	mathematical	ContinuousOn Set.uIoo Filter.Tendsto nhdsWithin nhds	extendFrom Set.uIcc DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	Ne.lt_or_gt Set.uIoo_of_lt Set.uIcc_of_lt continuousOn_Icc_extendFrom_Ioo nhdsWithin_Ioo_eq_nhdsGT instClosedIciTopology OrderTopology.to_orderClosedTopology nhdsWithin_Ioo_eq_nhdsLT instClosedIicTopology Set.uIoo_of_gt Set.uIcc_of_gt
eq_lim_at_left_extendFrom_Ioo 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Filter.Tendsto nhdsWithin Set.Ioi nhds	extendFrom Set.Ioo	—	extendFrom_eq closure_Ioo LT.lt.ne le_of_lt nhdsWithin_Ioo_eq_nhdsGT instClosedIciTopology OrderTopology.to_orderClosedTopology
eq_lim_at_left_extendFrom_uIoo 📖	mathematical	Filter.Tendsto nhdsWithin Set.uIoo nhds	extendFrom	—	extendFrom_eq closure_uIoo
eq_lim_at_right_extendFrom_Ioo 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Filter.Tendsto nhdsWithin Set.Iio nhds	extendFrom Set.Ioo	—	extendFrom_eq closure_Ioo LT.lt.ne le_of_lt nhdsWithin_Ioo_eq_nhdsLT instClosedIicTopology OrderTopology.to_orderClosedTopology
eq_lim_at_right_extendFrom_uIoo 📖	mathematical	Filter.Tendsto nhdsWithin Set.uIoo nhds	extendFrom	—	extendFrom_eq closure_uIoo

---

← Back to Index