HSpaces

📁 Source: Mathlib/Topology/Homotopy/HSpaces.lean

Statistics

Metric	Count
Definitions HSpace, e, eHmul, hmul, hmulE, prod, «term_⋀_», hSpace, toHSpace, hSpace, toHSpace, delayReflLeft, delayReflRight, instHSpace, qRight	15
Theorems hmul_e_e, one_eq_hSpace_e, continuous_delayReflLeft, continuous_delayReflRight, delayReflLeft_one, delayReflLeft_zero, delayReflRight_one, delayReflRight_zero, continuous_qRight, qRight_one_left, qRight_one_right, qRight_zero_left, qRight_zero_right	13
Total	28

HSpace

Definitions

Name	Category	Theorems
e 📖	CompOp	2 math math: hmul_e_e, IsTopologicalGroup.one_eq_hSpace_e
eHmul 📖	CompOp	—
hmul 📖	CompOp	1 math math: hmul_e_e
hmulE 📖	CompOp	—
prod 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hmul_e_e 📖	mathematical	—	DFunLike.coe ContinuousMap instTopologicalSpaceProd ContinuousMap.instFunLike hmul e	—	—

HSpaces

Definitions

Name	Category	Theorems
«term_⋀_» 📖	CompOp	—

IsTopologicalAddGroup

Definitions

Name	Category	Theorems
hSpace 📖	CompOp	—
toHSpace 📖	CompOp	—

IsTopologicalGroup

Definitions

Name	Category	Theorems
hSpace 📖	CompOp	1 math math: one_eq_hSpace_e
toHSpace 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
one_eq_hSpace_e 📖	mathematical	—	InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid HSpace.e hSpace	—	—

Path

Definitions

Name	Category	Theorems
delayReflLeft 📖	CompOp	3 math math: delayReflLeft_one, continuous_delayReflLeft, delayReflLeft_zero
delayReflRight 📖	CompOp	3 math math: delayReflRight_zero, continuous_delayReflRight, delayReflRight_one
instHSpace 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuous_delayReflLeft 📖	mathematical	—	Continuous Set.Elem Real unitInterval Path instTopologicalSpaceProd instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace instTopologicalSpace delayReflLeft	—	Continuous.comp continuous_symm continuous_delayReflRight Continuous.prodMk continuous_fst continuous_snd
continuous_delayReflRight 📖	mathematical	—	Continuous Set.Elem Real unitInterval Path instTopologicalSpaceProd instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace instTopologicalSpace delayReflRight	—	continuous_uncurry_iff Continuous.eval instContinuousEvalElemRealUnitInterval Continuous.comp continuous_snd continuous_fst unitInterval.continuous_qRight Continuous.prodMk
delayReflLeft_one 📖	mathematical	—	delayReflLeft Set.Elem Real unitInterval Set.Icc.instOne Real.semiring Real.partialOrder Real.instIsOrderedRing	—	Real.instIsOrderedRing delayReflRight_one symm_symm
delayReflLeft_zero 📖	mathematical	—	delayReflLeft Set.Elem Real unitInterval Set.Icc.instZero Real.semiring Real.partialOrder Real.instIsOrderedRing trans refl	—	Real.instIsOrderedRing delayReflRight_zero trans_symm symm_symm
delayReflRight_one 📖	mathematical	—	delayReflRight Set.Elem Real unitInterval Set.Icc.instOne Real.semiring Real.partialOrder Real.instIsOrderedRing	—	ext Real.instIsOrderedRing unitInterval.qRight_one_right
delayReflRight_zero 📖	mathematical	—	delayReflRight Set.Elem Real unitInterval Set.Icc.instZero Real.semiring Real.partialOrder Real.instIsOrderedRing trans refl	—	ext Real.instIsOrderedRing Nat.instAtLeastTwoHAddOfNat unitInterval.mul_pos_mem_iff zero_lt_two Real.instZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid unitInterval.two_mul_sub_one_mem_iff LT.lt.le not_le trans_apply unitInterval.qRight_zero_right target

(root)

Definitions

Name	Category	Theorems
HSpace 📖	CompData	—

unitInterval

Definitions

Name	Category	Theorems
qRight 📖	CompOp	5 math math: qRight_one_left, qRight_zero_right, continuous_qRight, qRight_zero_left, qRight_one_right

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuous_qRight 📖	mathematical	—	Continuous Set.Elem Real unitInterval instTopologicalSpaceProd instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace qRight	—	Continuous.comp continuous_projIcc instOrderTopologyReal Continuous.div IsTopologicalDivisionRing.toContinuousInv₀ instIsTopologicalDivisionRingReal IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Continuous.fun_mul continuous_const Continuous.comp' continuous_subtype_val Continuous.fst continuous_id' Continuous.fun_add IsTopologicalSemiring.toContinuousAdd Continuous.snd LT.lt.ne' add_pos zero_lt_one Real.instZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing
qRight_one_left 📖	mathematical	—	qRight Set.Elem Real unitInterval Set.Icc.instOne Real.semiring Real.partialOrder Real.instIsOrderedRing	—	Set.projIcc_of_right_le Real.instIsOrderedRing le_div_iff₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Real.instIsStrictOrderedRing add_pos zero_lt_one Real.instZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero Set.Icc.coe_one one_mul mul_one add_comm Nat.instAtLeastTwoHAddOfNat one_add_one_eq_two covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT AddRightCancelSemigroup.toIsRightCancelAdd contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le le_one
qRight_one_right 📖	mathematical	—	qRight Set.Elem Real unitInterval Set.Icc.instOne Real.semiring Real.partialOrder Real.instIsOrderedRing	—	Real.instIsOrderedRing zero_le_one Real.instZeroLEOneClass qRight.eq_1 Set.projIcc.congr_simp Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one mul_div_cancel_left₀ GroupWithZero.toMulDivCancelClass Mathlib.Meta.NormNum.isNat_eq_false IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing Nat.cast_zero Set.projIcc_val
qRight_zero_left 📖	mathematical	—	qRight Set.Elem Real unitInterval Set.Icc.instZero Real.semiring Real.partialOrder Real.instIsOrderedRing	—	Set.projIcc_of_le_left Real.instIsOrderedRing MulZeroClass.mul_zero zero_div
qRight_zero_right 📖	mathematical	—	Real Set Set.instMembership unitInterval qRight Set.Elem Set.Icc.instZero Real.semiring Real.partialOrder Real.instIsOrderedRing Real.instLE DivInvMonoid.toDiv Real.instDivInvMonoid Real.instOne instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.decidableLE Real.instMul	—	Real.instIsOrderedRing Nat.instAtLeastTwoHAddOfNat Set.projIcc.congr_simp add_zero div_one mul_pos_mem_iff zero_lt_two Real.instZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Set.projIcc_of_mem Set.right_mem_Icc LT.lt.le zero_lt_one Set.projIcc_eq_right le_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Linarith.add_neg CancelDenoms.derive_trans Mathlib.Meta.NormNum.IsNNRat.to_eq Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNNRat_inv_pos CancelDenoms.sub_subst CancelDenoms.div_subst Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNat_mul Mathlib.Tactic.Linarith.mul_neg Mathlib.Tactic.Linarith.sub_neg_of_lt lt_of_not_ge Mathlib.Meta.NormNum.isNat_lt_true

---

← Back to Index