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 Set.Icc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instTopologicalSpaceSubtype Set Set.instMembership 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 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 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 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 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 Set.Elem Set.Icc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instTopologicalSpaceSubtype Set Set.instMembership 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 Set.Elem Set.Icc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instTopologicalSpaceSubtype Set Set.instMembership concat IccInclusionRight	—	ext eq_or_ne Set.right_mem_Icc continuous_inclusion instReflLe 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	DFunLike.coe ContinuousMap Set.Elem Set.Icc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instTopologicalSpaceSubtype Set Set.instMembership instFunLike concat Preorder.toLE	—	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	DFunLike.coe ContinuousMap Set.Elem Set.Icc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instTopologicalSpaceSubtype Set Set.instMembership instFunLike concat Preorder.toLE	—	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	Filter.Tendsto ContinuousMap Set.Elem Set.Icc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instTopologicalSpaceSubtype Set Set.instMembership concat nhds compactOpen	—	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