Interval

📁 Source: Mathlib/Topology/ContinuousMap/Interval.lean

Statistics

Metric	Count
Definitions IccExtendCM, IccInclusionLeft, IccInclusionRight, concat, concatCM, projIccCM, Interval	7
Theorems IccExtendCM_of_mem, concatCM_left, concatCM_right, concat_comp_IccInclusionLeft, concat_comp_IccInclusionRight, concat_left, concat_right, tendsto_concat	8
Total	15

ContinuousMap

Definitions

Name	Category	Theorems
IccExtendCM 📖	CompOp	1 math math: IccExtendCM_of_mem
IccInclusionLeft 📖	CompOp	1 math math: concat_comp_IccInclusionLeft
IccInclusionRight 📖	CompOp	1 math math: concat_comp_IccInclusionRight
concat 📖	CompOp	5 math math: concat_right, concat_comp_IccInclusionLeft, concat_comp_IccInclusionRight, tendsto_concat, concat_left
concatCM 📖	CompOp	2 math math: concatCM_left, concatCM_right
projIccCM 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
IccExtendCM_of_mem 📖	mathematical	Set Set.instMembership Set.Icc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	DFunLike.coe ContinuousMap instFunLike Set.Elem instTopologicalSpaceSubtype compactOpen IccExtendCM	—	inf_of_le_right sup_of_le_right
concatCM_left 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set Set.instMembership Set.Icc	DFunLike.coe ContinuousMap Set.Elem instTopologicalSpaceSubtype instFunLike Top.top OrderTop.toTop Set.Icc.instOrderTopElemOfFactLe Bot.bot OrderBot.toBot Set.Icc.instOrderBotElemOfFactLe instTopologicalSpaceProd compactOpen concatCM	—	concat_left
concatCM_right 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Set Set.instMembership Set.Icc	DFunLike.coe ContinuousMap Set.Elem instTopologicalSpaceSubtype instFunLike Top.top OrderTop.toTop Set.Icc.instOrderTopElemOfFactLe Bot.bot OrderBot.toBot Set.Icc.instOrderBotElemOfFactLe instTopologicalSpaceProd compactOpen concatCM	—	concat_right
concat_comp_IccInclusionLeft 📖	mathematical	DFunLike.coe ContinuousMap Set.Elem Set.Icc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instTopologicalSpaceSubtype Set Set.instMembership instFunLike Top.top OrderTop.toTop Preorder.toLE Set.Icc.instOrderTopElemOfFactLe Bot.bot OrderBot.toBot Set.Icc.instOrderBotElemOfFactLe	comp concat IccInclusionLeft	—	ext continuous_inclusion Set.projIcc_val
concat_comp_IccInclusionRight 📖	mathematical	DFunLike.coe ContinuousMap Set.Elem Set.Icc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instTopologicalSpaceSubtype Set Set.instMembership instFunLike Top.top OrderTop.toTop Preorder.toLE Set.Icc.instOrderTopElemOfFactLe Bot.bot OrderBot.toBot Set.Icc.instOrderBotElemOfFactLe	comp concat IccInclusionRight	—	ext eq_or_ne Set.right_mem_Icc continuous_inclusion Set.projIcc_right LT.lt.not_ge lt_of_le_of_ne inf_of_le_right sup_of_le_right
concat_left 📖	mathematical	DFunLike.coe ContinuousMap Set.Elem Set.Icc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instTopologicalSpaceSubtype Set Set.instMembership instFunLike Top.top OrderTop.toTop Preorder.toLE Set.Icc.instOrderTopElemOfFactLe Bot.bot OrderBot.toBot Set.Icc.instOrderBotElemOfFactLe	concat	—	concat_comp_IccInclusionLeft
concat_right 📖	mathematical	DFunLike.coe ContinuousMap Set.Elem Set.Icc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instTopologicalSpaceSubtype Set Set.instMembership instFunLike Top.top OrderTop.toTop Preorder.toLE Set.Icc.instOrderTopElemOfFactLe Bot.bot OrderBot.toBot Set.Icc.instOrderBotElemOfFactLe	concat	—	concat_comp_IccInclusionRight
tendsto_concat 📖	mathematical	Filter.Eventually DFunLike.coe ContinuousMap Set.Elem Set.Icc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instTopologicalSpaceSubtype Set Set.instMembership instFunLike Top.top OrderTop.toTop Preorder.toLE Set.Icc.instOrderTopElemOfFactLe Bot.bot OrderBot.toBot Set.Icc.instOrderBotElemOfFactLe Filter.Tendsto nhds compactOpen	concat	—	tendsto_nhds_compactOpen Fact.out IsCompact.image IsCompact.inter_right isClosed_Iic instClosedIicTopology Subtype.instOrderClosedTopology OrderTopology.to_orderClosedTopology continuous_subtype_val continuous isClosed_Ici instClosedIciTopology concat_comp_IccInclusionLeft Set.MapsTo.comp inf_of_le_right sup_of_le_right concat_comp_IccInclusionRight Filter.mp_mem Filter.univ_mem' concat_left LT.lt.le concat_right

(root)

Definitions

Name	Category	Theorems
Interval 📖	CompOp	48 math math: Interval.div_bot, Interval.coe_sInf, Interval.coe_iInf₂, Interval.bot_add, Interval.length_sub_le, Interval.mem_pure, Interval.one_mem_one, Interval.coe_dual, Interval.subset_coe_map, Interval.dual_top, Interval.bot_mul, Interval.coe_zero, Interval.pure_zero, Interval.add_eq_zero_iff, Interval.dual_bot, Interval.length_sum_le, Interval.canLift, Interval.neg_bot, Interval.coe_iInf, Interval.sub_bot, Interval.add_bot, Interval.pure_injective, Interval.coe_top, Interval.dual_pure, Interval.coe_one, Interval.mul_bot, Interval.forall, Interval.bot_div, Interval.disjoint_coe, Interval.coe_subset_coe, Interval.length_zero, Interval.coe_sSubset_coe, Interval.coe_bot, Interval.inv_bot, Interval.instNontrivialOfNonempty, Interval.bot_sub, Interval.pure_one, Interval.zero_mem_zero, Interval.mul_eq_one_iff, Interval.length_neg, Interval.length_add_le, Interval.coe_inf, Interval.dual_map, Interval.exists, Interval.bot_pow, Interval.bot_nsmul, Interval.coe_pure, Interval.mem_pure_self

---

← Back to Index