Rolle

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

Statistics

Metric	Count
Definitions	0
Theorems exists_Ioo_extr_on_Icc, exists_isExtrOn_Ioo_of_tendsto, exists_isExtrOn_uIoo_of_tendsto, exists_isLocalExtr_Ioo, exists_isLocalExtr_Ioo_of_tendsto, exists_isLocalExtr_uIoo, exists_isLocalExtr_uIoo_of_tendsto, exists_uIoo_isExtrOn_uIcc	8
Total	8

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_Ioo_extr_on_Icc 📖	mathematical	Preorder.toLT PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ContinuousOn Set.Icc	Set Set.instMembership Set.Ioo IsExtrOn SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	Set.nonempty_Icc le_of_lt IsCompact.exists_isMinOn instClosedIicTopology OrderTopology.to_orderClosedTopology CompactIccSpace.isCompact_Icc ConditionallyCompleteLinearOrder.toCompactIccSpace IsCompact.exists_isMaxOn instClosedIciTopology le_antisymm Set.nonempty_Ioo Set.Ioo_subset_Icc_self lt_of_le_of_ne
exists_isExtrOn_Ioo_of_tendsto 📖	mathematical	Preorder.toLT PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ContinuousOn Set.Ioo Filter.Tendsto nhdsWithin Set.Ioi nhds Set.Iio	Set Set.instMembership IsExtrOn SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	extendFrom_extends T25Space.t2Space T3Space.t25Space T4Space.t3Space T5Space.toT4Space OrderTopology.t5Space exists_Ioo_extr_on_Icc continuousOn_Icc_extendFrom_Ioo T3Space.toRegularSpace LT.lt.ne eq_lim_at_left_extendFrom_Ioo eq_lim_at_right_extendFrom_Ioo IsExtrFilter.congr IsExtrOn.on_subset Set.Ioo_subset_Icc_self
exists_isExtrOn_uIoo_of_tendsto 📖	mathematical	ContinuousOn Set.uIoo ConditionallyCompleteLinearOrder.toLinearOrder Filter.Tendsto nhdsWithin nhds	Set Set.instMembership IsExtrOn PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	extendFrom_extends T25Space.t2Space T3Space.t25Space T4Space.t3Space T5Space.toT4Space OrderTopology.t5Space exists_uIoo_isExtrOn_uIcc continuousOn_uIcc_extendFrom_uIoo T3Space.toRegularSpace eq_lim_at_left_extendFrom_uIoo eq_lim_at_right_extendFrom_uIoo IsExtrFilter.congr IsExtrOn.on_subset Set.uIoo_subset_uIcc_self
exists_isLocalExtr_Ioo 📖	mathematical	Preorder.toLT PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ContinuousOn Set.Icc	Set Set.instMembership Set.Ioo IsLocalExtr SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	exists_Ioo_extr_on_Icc IsExtrOn.isLocalExtr Icc_mem_nhds OrderTopology.to_orderClosedTopology
exists_isLocalExtr_Ioo_of_tendsto 📖	mathematical	Preorder.toLT PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ContinuousOn Set.Ioo Filter.Tendsto nhdsWithin Set.Ioi nhds Set.Iio	Set Set.instMembership IsLocalExtr SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	exists_isExtrOn_Ioo_of_tendsto IsExtrOn.isLocalExtr Ioo_mem_nhds OrderTopology.to_orderClosedTopology
exists_isLocalExtr_uIoo 📖	mathematical	ContinuousOn Set.uIcc ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice	Set Set.instMembership Set.uIoo ConditionallyCompleteLinearOrder.toLinearOrder IsLocalExtr PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	exists_isLocalExtr_Ioo
exists_isLocalExtr_uIoo_of_tendsto 📖	mathematical	ContinuousOn Set.uIoo ConditionallyCompleteLinearOrder.toLinearOrder Filter.Tendsto nhdsWithin nhds	Set Set.instMembership IsLocalExtr PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	exists_isExtrOn_uIoo_of_tendsto IsExtrOn.isLocalExtr Ioo_mem_nhds OrderTopology.to_orderClosedTopology
exists_uIoo_isExtrOn_uIcc 📖	mathematical	ContinuousOn Set.uIcc ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice	Set Set.instMembership Set.uIoo ConditionallyCompleteLinearOrder.toLinearOrder IsExtrOn PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	exists_Ioo_extr_on_Icc

---

← Back to Index