UnitInterval

📁 Source: Mathlib/Topology/UnitInterval.lean

Statistics

Metric	Count
Definitions `addNSMul`, `convexCombo`, `convexCombo_assoc_coeff₁`, `convexCombo_assoc_coeff₁'`, `convexCombo_assoc_coeff₂`, `convexCombo_assoc_coeff₂'`, `tacticUnit_interval`, `iccHomeoI`, `unitInterval`, `instLinearOrderedCommMonoidWithZeroElemReal`, `submonoid`, `symmHomeomorph`, `termI`, `termσ`, `toNNReal`	15
Theorems `abs_sub_addNSMul_le`, `addNSMul_eq_right`, `addNSMul_zero`, `coe_convexCombo`, `convexCombo_assoc`, `convexCombo_assoc'`, `convexCombo_le`, `convexCombo_one`, `convexCombo_symm`, `convexCombo_zero`, `eq_convexCombo`, `le_convexCombo`, `monotone_addNSMul`, `abs_projIcc_sub_projIcc`, `affineHomeomorph_image_I`, `exists_monotone_Icc_subset_open_cover_Icc`, `exists_monotone_Icc_subset_open_cover_unitInterval`, `exists_monotone_Icc_subset_open_cover_unitInterval_prod_self`, `iccHomeoI_apply_coe`, `iccHomeoI_symm_apply_coe`, `projIcc_eq_one`, `projIcc_eq_zero`, `add_pos`, `coe_lt_one`, `coe_ne_one`, `coe_ne_zero`, `coe_pos`, `coe_symm_eq`, `coe_toNNReal`, `coe_unitIntervalSubmonoid`, `continuous_symm`, `div_mem`, `eq_closedBall`, `eq_one_or_eq_zero_of_le_mul`, `fract_mem`, `half_le_symm_iff`, `image_coe_preimage_symm`, `instConnectedSpaceElemReal`, `instNontrivialElemReal`, `le_one`, `le_one'`, `le_symm_comm`, `lt_one_iff_ne_one`, `lt_symm_comm`, `mem_unitIntervalSubmonoid`, `mul_le_left`, `mul_le_right`, `mul_mem`, `mul_pos_mem_iff`, `nonneg`, `nonneg'`, `one_mem`, `one_minus_le_one`, `one_minus_nonneg`, `pos_iff_ne_zero`, `prod_mem`, `strictAnti_symm`, `subtype_Ici_eq_Icc`, `subtype_Iic_eq_Icc`, `subtype_Iio_eq_Ico`, `subtype_Ioi_eq_Ioc`, `symmHomeomorph_apply`, `symmHomeomorph_symm_apply`, `symm_bijective`, `symm_eq_one`, `symm_eq_zero`, `symm_inj`, `symm_involutive`, `symm_le_comm`, `symm_le_symm`, `symm_lt_comm`, `symm_lt_symm`, `symm_one`, `symm_projIcc`, `symm_symm`, `symm_zero`, `toNNReal_add_toNNReal_symm`, `toNNReal_continuous`, `toNNReal_one`, `toNNReal_symm_add_toNNReal`, `toNNReal_zero`, `two_mul_sub_one_mem_iff`, `univ_eq_Icc`, `zero_mem`	84
Total	99

Set

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`abs_projIcc_sub_projIcc` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`abs` `AddCommGroup.toAddGroup` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `Set` `instMembership` `Icc` `projIcc`	—	`abs_eq_self` `sub_nonneg` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `monotone_projIcc` `LE.le.trans` `max_sub_max_le_max` `max_le` `sub_self` `le_abs_self` `abs_min_sub_min_le_max` `abs_zero` `Eq.le` `abs_sub_comm` `le_of_not_ge`

Set.Icc

Definitions

Name	Category	Theorems
`addNSMul` 📖	CompOp	3 math math: `addNSMul_eq_right`, `addNSMul_zero`, `monotone_addNSMul`
`convexCombo` 📖	CompOp	9 math math: `convexCombo_one`, `coe_convexCombo`, `eq_convexCombo`, `convexCombo_assoc`, `le_convexCombo`, `convexCombo_symm`, `convexCombo_assoc'`, `convexCombo_le`, `convexCombo_zero`
`convexCombo_assoc_coeff₁` 📖	CompOp	1 math math: `convexCombo_assoc`
`convexCombo_assoc_coeff₁'` 📖	CompOp	1 math math: `convexCombo_assoc'`
`convexCombo_assoc_coeff₂` 📖	CompOp	1 math math: `convexCombo_assoc`
`convexCombo_assoc_coeff₂'` 📖	CompOp	1 math math: `convexCombo_assoc'`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`abs_sub_addNSMul_le` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Set.Elem` `Set.Icc` `Set` `Set.instMembership` `Subtype.preorder` `addNSMul`	`abs` `AddCommGroup.toAddGroup` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid`	—	`abs_eq_self` `sub_nonneg` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `sub_le_sub_right` `le_abs_self` `Set.abs_projIcc_sub_projIcc` `add_sub_add_comm` `sub_self` `zero_add` `succ_nsmul'` `add_sub_cancel_right` `Eq.le`
`addNSMul_eq_right` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Preorder.toLT` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`Set` `Set.instMembership` `Set.Icc` `addNSMul`	—	`Archimedean.arch` `addNSMul.eq_1` `Set.coe_projIcc` `add_comm` `min_eq_left_iff` `sub_le_iff_le_add` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `LE.le.trans` `nsmul_le_nsmul_left` `LT.lt.le` `max_eq_right`
`addNSMul_zero` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Set` `Set.instMembership` `Set.Icc` `addNSMul`	—	`addNSMul.eq_1` `zero_smul` `add_zero` `Set.left_mem_Icc` `Set.projIcc_left`
`coe_convexCombo` 📖	mathematical	—	`Real` `Set` `Set.instMembership` `Set.Icc` `Real.instPreorder` `convexCombo` `Real.instAdd` `Real.instMul` `Real.instSub` `Real.instOne` `unitInterval`	—	—
`convexCombo_assoc` 📖	mathematical	—	`convexCombo` `convexCombo_assoc_coeff₁` `convexCombo_assoc_coeff₂`	—	`sub_self` `MulZeroClass.zero_mul` `one_mul` `zero_add` `mul_one` `MulZeroClass.mul_zero` `div_zero` `sub_zero` `add_zero` `Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.subst_add` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval` `Mathlib.Tactic.FieldSimp.subst_sub` `Mathlib.Tactic.FieldSimp.NF.one_eq_eval` `Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst` `div_one` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons` `Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div` `Mathlib.Tactic.FieldSimp.NF.eval_cons` `Mathlib.Tactic.FieldSimp.zpow'_one` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₂` `Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero` `Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial` `zero_div` `le_of_not_gt` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_pf_right` `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.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.cast_zero` `Nat.cast_zero` `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.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Real.instIsStrictOrderedRing` `Mathlib.Tactic.Linarith.lt_of_eq_of_lt` `sub_eq_zero_of_eq` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `Real.instIsOrderedRing` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `mul_nonneg_of_nonpos_of_nonpos` `AddGroup.existsAddOfLE` `IsOrderedRing.toMulPosMono` `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` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.RingNF.nat_rawCast_1` `pow_one` `Mathlib.Tactic.RingNF.int_rawCast_neg` `Mathlib.Tactic.RingNF.mul_neg` `Mathlib.Tactic.RingNF.mul_assoc_rev` `Mathlib.Tactic.RingNF.add_assoc_rev` `Mathlib.Tactic.RingNF.add_neg`
`convexCombo_assoc'` 📖	mathematical	—	`convexCombo` `convexCombo_assoc_coeff₂'` `convexCombo_assoc_coeff₁'`	—	`convexCombo_symm` `convexCombo_assoc` `convexCombo_assoc_coeff₁'.eq_1` `convexCombo_assoc_coeff₂'.eq_1` `unitInterval.symm_symm`
`convexCombo_le` 📖	mathematical	`Set.Elem` `Real` `Set.Icc` `Real.instPreorder` `Real.instLE` `Set` `Set.instMembership`	`convexCombo`	—	`Subtype.coe_le_coe` `le_of_not_gt` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_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_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Real.instIsStrictOrderedRing` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `Real.instIsOrderedRing` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `mul_nonneg_of_nonpos_of_nonpos` `AddGroup.existsAddOfLE` `IsOrderedRing.toMulPosMono` `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`
`convexCombo_one` 📖	mathematical	—	`convexCombo` `Set.Elem` `Real` `unitInterval` `instOne` `Real.semiring` `Real.partialOrder` `Real.instIsOrderedRing`	—	`Real.instIsOrderedRing` `sub_self` `MulZeroClass.zero_mul` `one_mul` `zero_add` `Subtype.coe_eta`
`convexCombo_symm` 📖	mathematical	—	`convexCombo` `unitInterval.symm`	—	`sub_sub_cancel` `Mathlib.Tactic.Abel.subst_into_addg` `Mathlib.Tactic.Abel.term_atomg` `Mathlib.Tactic.Abel.term_add_constg` `zero_add` `Mathlib.Tactic.Abel.const_add_termg` `add_zero`
`convexCombo_zero` 📖	mathematical	—	`convexCombo` `Set.Elem` `Real` `unitInterval` `instZero` `Real.semiring` `Real.partialOrder` `Real.instIsOrderedRing`	—	`Real.instIsOrderedRing` `sub_zero` `one_mul` `MulZeroClass.zero_mul` `add_zero` `Subtype.coe_eta`
`eq_convexCombo` 📖	mathematical	`Set.Elem` `Real` `Set.Icc` `Real.instPreorder` `Real.instLE` `Set` `Set.instMembership`	`convexCombo` `unitInterval` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instSub` `Preorder.toLE` `Real.instZero` `Real.instOne`	—	`div_zero` `sub_zero` `one_mul` `MulZeroClass.zero_mul` `add_zero` `Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.atom_pf` `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_zero` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.cast_zero` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_zero` `Mathlib.Tactic.Linarith.add_lt_of_le_of_neg` `Real.instIsStrictOrderedRing` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `Real.instIsOrderedRing` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `Mathlib.Tactic.Linarith.le_of_eq_of_le` `sub_eq_zero_of_eq` `Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons` `Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst` `Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div` `div_one` `Mathlib.Tactic.FieldSimp.NF.eval_cons` `Mathlib.Tactic.FieldSimp.zpow'_one` `Mathlib.Tactic.FieldSimp.subst_add` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval` `Mathlib.Tactic.FieldSimp.subst_sub` `Mathlib.Tactic.FieldSimp.NF.one_eq_eval` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `mul_one` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁` `Mathlib.Tactic.FieldSimp.NF.cons_ne_zero` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.RingNF.nat_rawCast_1` `pow_one` `Mathlib.Tactic.RingNF.int_rawCast_neg` `Mathlib.Tactic.RingNF.mul_neg` `Mathlib.Tactic.RingNF.add_neg` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Tactic.Ring.mul_one`
`le_convexCombo` 📖	mathematical	`Set.Elem` `Real` `Set.Icc` `Real.instPreorder` `Real.instLE` `Set` `Set.instMembership`	`convexCombo`	—	`Subtype.coe_le_coe` `le_of_not_gt` `Mathlib.Tactic.Linarith.lt_irrefl` `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.atom_pf` `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_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Real.instIsStrictOrderedRing` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `Real.instIsOrderedRing` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `mul_nonneg_of_nonpos_of_nonpos` `AddGroup.existsAddOfLE` `IsOrderedRing.toMulPosMono` `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`
`monotone_addNSMul` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`Monotone` `Set.Elem` `Set.Icc` `Nat.instPreorder` `Subtype.preorder` `Set` `Set.instMembership` `addNSMul`	—	`Set.monotone_projIcc` `add_le_add_iff_left` `IsOrderedAddMonoid.toAddLeftMono` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `nsmul_le_nsmul_left`

Tactic.Interactive

Definitions

Name	Category	Theorems
`tacticUnit_interval` 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
`iccHomeoI` 📖	CompOp	3 math math: `iccHomeoI_apply_coe`, `iccHomeoI_symm_apply_coe`, `polynomialFunctions.comap_compRightAlgHom_iccHomeoI`
`unitInterval` 📖	CompOp	310 math math: `ContinuousMap.HomotopyRel.prod_apply`, `completelyRegularSpace_iff_isOpen`, `Path.subpath_self`, `IsPathConnected.exists_path_through_family'`, `bernsteinApproximation.apply_zero`, `unitInterval.sigmoid_le_iff`, `unitInterval.symmHomeomorph_apply`, `Path.continuousMapClass`, `unitInterval.volume_Ioo`, `unitInterval.volume_Iic`, `ContinuousMap.HomotopyWith.coe_toContinuousMap`, `unitInterval.volume_def`, `unitInterval.sigmoid_lt`, `unitInterval.zero_mem`, `unitInterval.strictAnti_symm`, `Metric.PiNatEmbed.continuous_distDenseSeq_inv`, `ProbabilityTheory.unitInterval.cdf_eq_real`, `Path.extend_extends`, `GenLoop.fromLoop_apply`, `stdSimplexHomeomorphUnitInterval_symm_apply_coe`, `unitInterval.toNNReal_continuous`, `unitInterval.measurePreserving_coe`, `ContinuousMap.Homotopy.apply_zero_path`, `selfAdjoint.expUnitaryPathToOne_apply`, `HomotopyGroup.symmAt_indep`, `ContDiffPointwiseHolderAt.isBigO`, `ContinuousMap.HomotopyWith.prop'`, `unitInterval.pos_iff_ne_zero`, `Path.Homotopy.map_apply`, `Path.pi_coe`, `unitInterval.coe_symmMeasurableEquiv`, `Path.range_subpathAux`, `unitInterval.volume_Ico`, `Path.ext_iff`, `ContinuousMap.HomotopyLike.map_zero_left`, `ContinuousMap.Homotopy.evalAt_eq`, `unitInterval.volume_apply`, `unitInterval.sigmoid_strictMono`, `unitInterval.symm_le_symm`, `stdSimplexHomeomorphUnitInterval_zero`, `GenLoop.homotopyTo_apply`, `Path.Homotopy.continuous_transAssocReparamAux`, `Path.Homotopy.target`, `unitInterval.symmMeasurableEquiv_apply`, `HomotopyGroup.isUnital_auxGroup`, `unitInterval.mem_unitIntervalSubmonoid`, `Path.delayReflRight_zero`, `ContinuousMap.HomotopyWith.apply_one`, `Path.Homotopy.eval_zero`, `ContinuousMap.HomotopyRel.refl_apply`, `unitInterval.qRight_one_left`, `ContinuousMap.Homotopy.ulift_apply`, `GenLoop.loopHomeo_apply`, `Path.delayReflLeft_one`, `ProbabilityTheory.setBernoulli_one`, `ContinuousMap.HomotopyRel.trans_apply`, `Path.Homotopy.reflTransSymmAux_mem_I`, `ContinuousMap.Homotopy.cast_apply`, `Path.toHomotopyConst_apply`, `unitInterval.measurePreserving_symm`, `Path.extend_apply`, `measurableEmbedding_sigmoid`, `HomotopyGroup.transAt_indep`, `unitInterval.toNNReal_zero`, `ContinuousMap.Homotopy.compContinuousMap_apply`, `Path.cast_coe`, `ContinuousMap.Homotopy.comp_apply`, `Path.subpathAux_one`, `Path.continuous_delayReflRight`, `unitInterval.lt_one_iff_ne_one`, `measurableEmbedding_sigmoid_comp_embeddingReal`, `unitInterval.lt_symm_comm`, `GenLoop.instContinuousEval`, `Path.Homotopy.hcomp_half`, `Set.Icc.convexCombo_one`, `Path.Homotopy.hcomp_apply`, `Path.continuous_delayReflLeft`, `Path.Homotopy.symm_apply`, `unitInterval.volume_uIcc`, `Path.instContinuousEvalElemRealUnitInterval`, `Path.Homotopy.transAssocReparamAux_mem_I`, `unitInterval.volume_Ici`, `Path.Homotopy.eval_apply`, `Path.Homotopy.transAssocReparamAux_zero`, `IsPathConnected.exists_path_through_family`, `ContinuousMap.Homotopy.apply_one_path`, `unitInterval.volume_uIoo`, `IsCoveringMap.liftPath_const`, `ContinuousMap.HomotopyRel.compContinuousMap_apply`, `Path.mul_apply`, `ContinuousMap.HomotopyLike.toContinuousMapClass`, `bernstein.variance`, `bernstein_apply`, `GenLoop.ext_iff`, `unitInterval.measurable_symm`, `Metric.PiNatEmbed.separation`, `unitInterval.continuous_sigmoid`, `ContinuousMap.HomotopyWith.coeFn_injective`, `Path.Homotopy.transAssocReparamAux_one`, `Path.Homotopy.transReflReparamAux_one`, `unitInterval.one_minus_le_one`, `ContinuousMap.Homotopy.extend_apply_coe`, `Set.Icc.coe_convexCombo`, `ContinuousMap.Homotopy.evalAt_apply`, `ContinuousMap.Homotopy.symm_apply`, `unitInterval.volume_Icc`, `unitInterval.range_sigmoid`, `Path.source'`, `unitInterval.coe_unitIntervalSubmonoid`, `unitInterval.mul_le_left`, `GenLoop.continuous_fromLoop`, `contDiffPointwiseHolderAt_iff`, `Path.reparam_id`, `Path.uniformContinuous`, `ContinuousMap.HomotopyWith.trans_apply`, `Set.Icc.eq_convexCombo`, `GenLoop.toLoop_apply`, `unitInterval.one_mem`, `unitInterval.fract_mem`, `Path.Homotopy.trans_assoc_reparam`, `HomotopyGroup.mul_spec`, `Path.extend_range`, `unitInterval.symm_one`, `GenLoop.fromLoop_symm_toLoop`, `Path.delayReflLeft_zero`, `unitInterval.coe_symm_eq`, `unitInterval.symmMeasurableEquiv_symm_apply`, `unitInterval.qRight_zero_right`, `unitInterval.mul_le_right`, `Path.isUniformEmbedding_coe`, `unitInterval.symmHomeomorph_symm_apply`, `Path.range_subpath`, `unitInterval.continuous_qRight`, `Path.symm_apply`, `unitInterval.nonneg'`, `unitInterval.le_one'`, `Path.Homotopy.trans_apply`, `unitInterval.symm_le_comm`, `Metric.PiNatEmbed.exists_closed_embedding_to_hilbert_cube`, `unitInterval.instTietzeExtension`, `Path.Homotopy.continuous_reflTransSymmAux`, `Path.inv_apply`, `ContinuousMap.Homotopy.trans_apply`, `unitInterval.div_mem`, `ContinuousMap.HomotopyRel.symm_apply`, `Path.refl_apply`, `Path.range_segment`, `ProbabilityTheory.setBernoulli_zero`, `Path.continuous_uncurry_iff`, `unitInterval.qRight_zero_left`, `bernsteinApproximation.apply_one`, `Path.prod_coe`, `bernstein_nonneg`, `Manifold.riemannianEDist_def`, `unitInterval.le_one`, `curveIntegralFun_def'`, `unitInterval.instIsProbabilityMeasureElemRealVolume`, `unitInterval.symm_eq_zero`, `stdSimplexHomeomorphUnitInterval_apply_coe`, `ContinuousMap.Homotopy.curry_apply`, `unitInterval.mul_pos_mem_iff`, `unitInterval.sigmoid_injective`, `Path.Homotopy.transReflReparamAux_zero`, `Path.Homotopy.cast_apply`, `GenLoop.toLoop_apply_coe`, `Metric.PiNatEmbed.continuous_distDenseSeq`, `bernstein.z_zero`, `Path.Homotopy.coeFn_injective`, `unitInterval.image_coe_preimage_symm`, `Real.fromBinary_surjective`, `CompletelyRegularSpace.completely_regular`, `GenLoop.loopHomeo_symm_apply`, `ContinuousMap.HomotopyWith.ext_iff`, `Path.continuous`, `Path.source_mem_range`, `ContinuousMap.HomotopyLike.map_one_left`, `Path.neg_apply`, `Path.target_mem_range`, `unitInterval.tendsto_sigmoid_atTop`, `PathConnectedSpace.exists_path_through_family`, `unitInterval.symm_zero`, `Path.subpathAux_continuous`, `unitInterval.subtype_Ici_eq_Icc`, `unitInterval.symm_lt_comm`, `unitInterval.coe_lt_one`, `unitInterval.sigmoid_lt_iff`, `unitInterval.subtype_Iio_eq_Ico`, `HomotopyGroup.one_def`, `Path.target'`, `unitInterval.volume_Ioc`, `unitInterval.coe_pos`, `stdSimplexHomeomorphUnitInterval_one`, `ContinuousMap.Homotopy.continuous`, `Path.trans_apply`, `ContinuousMap.Homotopy.affine_apply`, `Path.trans_range`, `Path.symm_subpath`, `HomotopyGroup.inv_spec`, `PathConnectedSpace.exists_path_through_family'`, `Path.range_coe`, `separatesPoints_continuous_of_t35Space_Icc`, `Path.Homotopy.transReflReparamAux_mem_I`, `Path.add_apply`, `Path.map_coe`, `ContinuousMap.Homotopy.coe_toContinuousMap`, `ContinuousMap.Homotopy.apply_zero`, `Path.subpath_continuous_family`, `JoinedIn.somePath_mem`, `Path.Homotopy.continuous_transReflReparamAux`, `cantorToHilbert_continuous`, `ContinuousMap.Homotopy.prod_apply`, `Path.refl_range`, `ContinuousMap.HomotopyWith.prop`, `Path.id_apply`, `ContinuousMap.HomotopyWith.refl_apply`, `unitInterval.coe_toNNReal`, `Path.source`, `Path.coe_toContinuousMap`, `bernsteinApproximation_uniform`, `ContinuousMap.Homotopy.map_one_left`, `ContinuousMap.Homotopy.apply_one`, `GenLoop.Homotopic.equiv`, `Path.truncate_const_continuous_family`, `unitInterval.measurableEmbedding_coe`, `unitInterval.sigmoid_monotone`, `Path.Homotopy.trans_refl_reparam`, `ContinuousMap.Homotopy.congr_fun`, `Path.extend_extends'`, `unitInterval.instNoAtomsElemRealVolume`, `Path.truncate_continuous_family`, `unitInterval.nonneg`, `ContinuousMap.HomotopyWith.symm_apply`, `ContinuousMap.HomotopyWith.continuous`, `unitInterval.one_minus_nonneg`, `unitInterval.symm_lt_symm`, `ContinuousMap.Homotopy.ext_iff`, `Path.delayReflRight_one`, `ContinuousMap.HomotopyRel.cast_apply`, `Path.subpathAux_zero`, `ContinuousMap.HomotopyWith.coe_toHomotopy`, `Path.Homotopy.eval_one`, `ContinuousMap.HomotopyRel.eq_fst`, `Path.target`, `unitInterval.instNontrivialElemReal`, `Path.Homotopy.source`, `polynomialFunctions_closure_eq_top'`, `bernstein.z_last`, `bernstein.probability`, `completelyRegularSpace_iff`, `unitInterval.univ_eq_Icc`, `unitInterval.subtype_Iic_eq_Icc`, `unitInterval.eq_closedBall`, `ContinuousMap.HomotopyWith.apply_zero`, `unitInterval.half_le_symm_iff`, `ContinuousMap.Homotopy.refl_apply`, `ContinuousMap.HomotopyWith.cast_apply`, `unitInterval.sigmoid_pos`, `unitInterval.symm_involutive`, `Path.subpath_zero_one`, `unitInterval.volume_uIoc`, `Topology.isEmbedding_sigmoid`, `Path.segment_apply`, `Path.Homotopy.symm₂_apply`, `unitInterval.add_pos`, `ContDiffPointwiseHolderAt.zero_exponent_iff`, `unitInterval.tendsto_sigmoid_atBot`, `ContinuousMap.Homotopy.curry_one`, `unitInterval.subtype_Ioi_eq_Ioc`, `ContinuousMap.HomotopyRel.pi_apply`, `unitInterval.two_mul_sub_one_mem_iff`, `unitInterval.symm_eq_one`, `Path.Homotopy.refl_apply`, `unitInterval.symm_bijective`, `Path.symm_range`, `unitInterval.sigmoid_lt_one`, `ContDiffPointwiseHolderAt.zero_order_iff`, `GenLoop.boundary`, `GenLoop.homotopyFrom_apply`, `GenLoop.const_apply`, `GenLoop.fromLoop_coe`, `unitInterval.sigmoid_le`, `unitInterval.qRight_one_right`, `GenLoop.homotopicTo`, `GenLoop.continuous_toLoop`, `ContinuousMap.Homotopy.congr_arg`, `unitInterval.le_symm_comm`, `GenLoop.fromLoop_trans_toLoop`, `Real.fromBinary_continuous`, `Unitary.path_apply`, `curveIntegralFun_def`, `Path.truncate_range`, `ContinuousMap.Homotopy.map_zero_left`, `unitInterval.continuous_symm`, `unitInterval.toNNReal_one`, `unitInterval.symm_symmMeasurableEquiv`, `Path.Homotopic.concat_subpath`, `Path.eqOn_extend_segment`, `GenLoop.instContinuousEvalConst`, `CompletelyRegularSpace.completely_regular_isOpen`, `unitInterval.volume_Iio`, `Set.Icc.convexCombo_zero`, `ContinuousMap.HomotopyRel.eq_snd`, `bernsteinApproximation.apply`, `ContinuousMap.Homotopy.curry_zero`, `Metric.PiNatEmbed.exists_embedding_to_hilbert_cube`, `polynomialFunctions.comap_compRightAlgHom_iccHomeoI`, `unitInterval.instConnectedSpaceElemReal`, `IsCoveringMap.liftPath_trans`, `isSimplyConnected_iff_exists_homotopy_refl_forall_mem`, `unitInterval.volume_Ioi`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`affineHomeomorph_image_I` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing`	`Set.image` `DFunLike.coe` `Homeomorph` `EquivLike.toFunLike` `Homeomorph.instEquivLike` `affineHomeomorph` `LT.lt.ne` `Set.Icc` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib`	—	`LT.lt.ne` `Set.image_congr` `Set.image_affine_Icc'` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `AddGroup.existsAddOfLE` `MulZeroClass.mul_zero` `zero_add` `mul_one`
`exists_monotone_Icc_subset_open_cover_Icc` 📖	mathematical	`Real` `Real.instLE` `IsOpen` `Set.Elem` `Set.Icc` `Real.instPreorder` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Set.instHasSubset` `Set.univ` `Set.iUnion`	`Monotone` `Nat.instPreorder` `Subtype.preorder`	—	`lebesgue_number_lemma_of_metric` `isCompact_univ` `compactSpace_Icc` `ConditionallyCompleteLinearOrder.toCompactIccSpace` `instOrderTopologyReal` `Nat.instAtLeastTwoHAddOfNat` `half_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Set.Icc.addNSMul_zero` `Set.Icc.monotone_addNSMul` `Real.instIsOrderedAddMonoid` `LT.lt.le` `Set.Icc.addNSMul_eq_right` `Real.instArchimedean` `LE.le.trans_lt` `Set.Icc.abs_sub_addNSMul_le` `half_lt_self`
`exists_monotone_Icc_subset_open_cover_unitInterval` 📖	mathematical	`IsOpen` `Set.Elem` `Real` `unitInterval` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Set.instHasSubset` `Set.univ` `Set.iUnion`	`Set.Icc.instZero` `Real.semiring` `Real.partialOrder` `Real.instIsOrderedRing` `Monotone` `Nat.instPreorder` `Subtype.preorder` `Real.instPreorder` `Set.Icc.instOne` `Set.Icc`	—	`Real.instIsOrderedRing` `exists_monotone_Icc_subset_open_cover_Icc` `zero_le_one` `Real.instZeroLEOneClass`
`exists_monotone_Icc_subset_open_cover_unitInterval_prod_self` 📖	mathematical	`IsOpen` `Set.Elem` `Real` `unitInterval` `instTopologicalSpaceProd` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Set.instHasSubset` `Set.univ` `Set.iUnion`	`Set.Icc.instZero` `Real.semiring` `Real.partialOrder` `Real.instIsOrderedRing` `Monotone` `Nat.instPreorder` `Subtype.preorder` `Real.instPreorder` `Set.Icc.instOne` `SProd.sprod` `Set.instSProd` `Set.Icc`	—	`Real.instIsOrderedRing` `lebesgue_number_lemma_of_metric` `isCompact_univ` `instCompactSpaceProd` `compactSpace_Icc` `ConditionallyCompleteLinearOrder.toCompactIccSpace` `instOrderTopologyReal` `Nat.instAtLeastTwoHAddOfNat` `half_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `zero_le_one` `Real.instZeroLEOneClass` `Set.Icc.addNSMul_zero` `Set.Icc.monotone_addNSMul` `Real.instIsOrderedAddMonoid` `LT.lt.le` `Set.Icc.addNSMul_eq_right` `Real.instArchimedean` `Metric.mem_ball` `LE.le.trans_lt` `max_le` `Set.Icc.abs_sub_addNSMul_le` `half_lt_self`
`iccHomeoI_apply_coe` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Set` `Set.instMembership` `Set.Icc` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `DFunLike.coe` `Homeomorph` `Set.Elem` `instTopologicalSpaceSubtype` `EquivLike.toFunLike` `Homeomorph.instEquivLike` `iccHomeoI` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup`	—	—
`iccHomeoI_symm_apply_coe` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Set` `Set.instMembership` `Set.Icc` `DFunLike.coe` `Homeomorph` `Set.Elem` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `instTopologicalSpaceSubtype` `EquivLike.toFunLike` `Homeomorph.instEquivLike` `Homeomorph.symm` `iccHomeoI` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `Distrib.toMul` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup`	—	—
`projIcc_eq_one` 📖	mathematical	—	`Set.projIcc` `Real` `Real.linearOrder` `Real.instZero` `Real.instOne` `zero_le_one` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Real.instZeroLEOneClass` `Set.Elem` `Set.Icc` `Set.Icc.instOne` `Real.semiring` `Real.partialOrder` `Real.instIsOrderedRing` `Real.instLE`	—	`Set.projIcc_eq_right` `zero_lt_one` `Real.instZeroLEOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing`
`projIcc_eq_zero` 📖	mathematical	—	`Set.projIcc` `Real` `Real.linearOrder` `Real.instZero` `Real.instOne` `zero_le_one` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Real.instZeroLEOneClass` `Set.Elem` `Set.Icc` `Set.Icc.instZero` `Real.semiring` `Real.partialOrder` `Real.instIsOrderedRing` `Real.instLE`	—	`Set.projIcc_eq_left` `zero_lt_one` `Real.instZeroLEOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing`

unitInterval

Definitions

Name	Category	Theorems
`instLinearOrderedCommMonoidWithZeroElemReal` 📖	CompOp	—
`submonoid` 📖	CompOp	2 math math: `mem_unitIntervalSubmonoid`, `coe_unitIntervalSubmonoid`
`symmHomeomorph` 📖	CompOp	2 math math: `symmHomeomorph_apply`, `symmHomeomorph_symm_apply`
`termI` 📖	CompOp	—
`termσ` 📖	CompOp	—
`toNNReal` 📖	CompOp	11 math math: `toNNReal_continuous`, `ProbabilityTheory.setBernoulli_singleton`, `toNNReal_zero`, `ProbabilityTheory.setBernoulli_apply'`, `MeasureTheory.instIsProbabilityMeasureHAddMeasureHSMulNNRealToNNRealSymm`, `coe_toNNReal`, `toNNReal_symm_add_toNNReal`, `ProbabilityTheory.setBernoulli_apply`, `toNNReal_add_toNNReal_symm`, `toNNReal_one`, `ProbabilityTheory.setBernoulli_eq_map`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_pos` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`Real.instAdd` `Set` `Set.instMembership` `unitInterval`	—	`add_pos_of_pos_of_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `nonneg`
`coe_lt_one` 📖	mathematical	—	`Real` `Real.instLT` `Set` `Set.instMembership` `unitInterval` `Real.instOne` `Set.Elem` `Set.Icc.instOne` `Real.semiring` `Real.partialOrder` `Real.instIsOrderedRing`	—	—
`coe_ne_one` 📖	—	—	—	—	`Iff.not` `Real.instIsOrderedRing` `Set.Icc.coe_eq_one`
`coe_ne_zero` 📖	—	—	—	—	`Iff.not` `Real.instIsOrderedRing` `Set.Icc.coe_eq_zero`
`coe_pos` 📖	mathematical	—	`Real` `Real.instLT` `Real.instZero` `Set` `Set.instMembership` `unitInterval` `Set.Elem` `Set.Icc.instZero` `Real.semiring` `Real.partialOrder` `Real.instIsOrderedRing`	—	—
`coe_symm_eq` 📖	mathematical	—	`Real` `Set` `Set.instMembership` `unitInterval` `symm` `Real.instSub` `Real.instOne`	—	—
`coe_toNNReal` 📖	mathematical	—	`NNReal.toReal` `toNNReal` `Real` `Set` `Set.instMembership` `unitInterval`	—	—
`coe_unitIntervalSubmonoid` 📖	mathematical	—	`SetLike.coe` `Submonoid` `Real` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `Real.semiring` `Submonoid.instSetLike` `submonoid` `unitInterval`	—	—
`continuous_symm` 📖	mathematical	—	`Continuous` `Set.Elem` `Real` `unitInterval` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `symm`	—	`Continuous.sub` `IsTopologicalAddGroup.to_continuousSub` `instIsTopologicalAddGroupReal` `continuous_const` `continuous_subtype_val`
`div_mem` 📖	mathematical	`Real` `Real.instLE` `Real.instZero`	`Set` `Set.instMembership` `unitInterval` `DivInvMonoid.toDiv` `Real.instDivInvMonoid`	—	`div_nonneg` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `div_le_one_of_le₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `Real.instZeroLEOneClass`
`eq_closedBall` 📖	mathematical	—	`unitInterval` `Metric.closedBall` `Real` `Real.pseudoMetricSpace` `Real.instInv` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Real.Icc_eq_closedBall` `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.isNat_add` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_zero` `Nat.cast_one` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_sub` `Mathlib.Meta.NormNum.IsNat.to_isInt`
`eq_one_or_eq_zero_of_le_mul` 📖	mathematical	`Set.Elem` `Real` `unitInterval` `Real.instLE` `Set` `Set.instMembership` `Set.Icc.instMul` `Real.semiring` `Real.partialOrder` `Real.instIsOrderedRing`	`Set.Icc.instZero` `Set.Icc.instOne`	—	`Real.instIsOrderedRing` `Mathlib.Tactic.Contrapose.contrapose₁` `Subtype.coe_lt_coe` `Set.Icc.coe_mul` `one_mul` `mul_lt_mul_of_pos_right` `IsStrictOrderedRing.toMulPosStrictMono` `Real.instIsStrictOrderedRing` `coe_pos` `pos_iff_ne_zero` `coe_lt_one` `lt_one_iff_ne_one`
`fract_mem` 📖	mathematical	—	`Real` `Set` `Set.instMembership` `unitInterval` `Int.fract` `Real.instRing` `Real.linearOrder` `Real.instFloorRing`	—	`Int.fract_nonneg` `Real.instIsStrictOrderedRing` `LT.lt.le` `Int.fract_lt_one`
`half_le_symm_iff` 📖	mathematical	—	`Real` `Real.instLE` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instOne` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Set` `Set.instMembership` `unitInterval` `symm`	—	`Nat.instAtLeastTwoHAddOfNat` `coe_symm_eq` `le_sub_iff_add_le` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `add_comm` `sub_half` `CharZero.NeZero.two` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing`
`image_coe_preimage_symm` 📖	mathematical	—	`Set.image` `Real` `Set` `Set.instMembership` `unitInterval` `Set.preimage` `Set.Elem` `symm` `Real.instSub` `Real.instOne`	—	`Set.image_image` `Set.image_congr`
`instConnectedSpaceElemReal` 📖	mathematical	—	`ConnectedSpace` `Set.Elem` `Real` `unitInterval` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace`	—	`Subtype.connectedSpace` `Set.nonempty_Icc` `zero_le_one` `Real.instZeroLEOneClass` `isPreconnected_Icc` `instOrderTopologyReal` `LinearOrderedSemiField.toDenselyOrdered` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing`
`instNontrivialElemReal` 📖	mathematical	—	`Nontrivial` `Set.Elem` `Real` `unitInterval`	—	`Real.instIsOrderedRing` `one_ne_zero` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing`
`le_one` 📖	mathematical	—	`Real` `Real.instLE` `Set` `Set.instMembership` `unitInterval` `Real.instOne`	—	—
`le_one'` 📖	mathematical	—	`Set.Elem` `Real` `unitInterval` `Real.instLE` `Set` `Set.instMembership` `Set.Icc.instOne` `Real.semiring` `Real.partialOrder` `Real.instIsOrderedRing`	—	—
`le_symm_comm` 📖	mathematical	—	`Set.Elem` `Real` `unitInterval` `Real.instLE` `Set` `Set.instMembership` `symm`	—	`symm_le_symm` `symm_symm`
`lt_one_iff_ne_one` 📖	mathematical	—	`Set.Elem` `Real` `unitInterval` `Real.instLT` `Set` `Set.instMembership` `Set.Icc.instOne` `Real.semiring` `Real.partialOrder` `Real.instIsOrderedRing`	—	`lt_top_iff_ne_top` `ZeroLEOneClass.factZeroLeOne` `Real.instZeroLEOneClass`
`lt_symm_comm` 📖	mathematical	—	`Set.Elem` `Real` `unitInterval` `Real.instLT` `Set` `Set.instMembership` `symm`	—	`symm_lt_symm` `symm_symm`
`mem_unitIntervalSubmonoid` 📖	mathematical	—	`Real` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `Real.semiring` `SetLike.instMembership` `Submonoid.instSetLike` `submonoid` `Set` `Set.instMembership` `unitInterval`	—	—
`mul_le_left` 📖	mathematical	—	`Set.Elem` `Real` `unitInterval` `Real.instLE` `Set` `Set.instMembership` `Set.Icc.instMul` `Real.semiring` `Real.partialOrder` `Real.instIsOrderedRing`	—	`Real.instIsOrderedRing` `Subtype.coe_le_coe` `mul_le_of_le_one_right` `IsOrderedRing.toPosMulMono`
`mul_le_right` 📖	mathematical	—	`Set.Elem` `Real` `unitInterval` `Real.instLE` `Set` `Set.instMembership` `Set.Icc.instMul` `Real.semiring` `Real.partialOrder` `Real.instIsOrderedRing`	—	`Real.instIsOrderedRing` `Subtype.coe_le_coe` `mul_le_of_le_one_left` `IsOrderedRing.toMulPosMono`
`mul_mem` 📖	mathematical	`Real` `Set` `Set.instMembership` `unitInterval`	`Real.instMul`	—	`mul_nonneg` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `mul_le_one₀` `IsOrderedRing.toMulPosMono`
`mul_pos_mem_iff` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`Set` `Set.instMembership` `unitInterval` `Real.instMul` `Set.Icc` `Real.instPreorder` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instOne`	—	`nonneg_of_mul_nonneg_right` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `le_div_iff₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `mul_comm` `mul_nonneg` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `LT.lt.le`
`nonneg` 📖	mathematical	—	`Real` `Real.instLE` `Real.instZero` `Set` `Set.instMembership` `unitInterval`	—	—
`nonneg'` 📖	mathematical	—	`Set.Elem` `Real` `unitInterval` `Real.instLE` `Set` `Set.instMembership` `Set.Icc.instZero` `Real.semiring` `Real.partialOrder` `Real.instIsOrderedRing`	—	—
`one_mem` 📖	mathematical	—	`Real` `Set` `Set.instMembership` `unitInterval` `Real.instOne`	—	`zero_le_one` `Real.instZeroLEOneClass` `le_rfl`
`one_minus_le_one` 📖	mathematical	—	`Real` `Real.instLE` `Real.instSub` `Real.instOne` `Set` `Set.instMembership` `unitInterval`	—	`AddGroup.toOrderedSub` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le`
`one_minus_nonneg` 📖	mathematical	—	`Real` `Real.instLE` `Real.instZero` `Real.instSub` `Real.instOne` `Set` `Set.instMembership` `unitInterval`	—	`covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid`
`pos_iff_ne_zero` 📖	mathematical	—	`Set.Elem` `Real` `unitInterval` `Real.instLT` `Set` `Set.instMembership` `Set.Icc.instZero` `Real.semiring` `Real.partialOrder` `Real.instIsOrderedRing`	—	`bot_lt_iff_ne_bot` `ZeroLEOneClass.factZeroLeOne` `Real.instZeroLEOneClass`
`prod_mem` 📖	mathematical	`Real` `Set` `Set.instMembership` `unitInterval`	`Finset.prod` `Real.instCommMonoid`	—	`prod_mem` `Submonoid.instSubmonoidClass`
`strictAnti_symm` 📖	mathematical	—	`StrictAnti` `Set.Elem` `Real` `unitInterval` `Subtype.preorder` `Real.instPreorder` `Set` `Set.instMembership` `symm`	—	`sub_lt_sub_left` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add`
`subtype_Ici_eq_Icc` 📖	mathematical	—	`Set.preimage` `Real` `Set` `Set.instMembership` `unitInterval` `Set.Ici` `Real.instPreorder` `Set.Icc` `Set.Elem` `Subtype.preorder` `Set.Icc.instOne` `Real.semiring` `Real.partialOrder` `Real.instIsOrderedRing`	—	`Real.instIsOrderedRing` `Set.preimage_subtype_val_Ici` `ZeroLEOneClass.factZeroLeOne` `Real.instZeroLEOneClass` `Set.Icc_top`
`subtype_Iic_eq_Icc` 📖	mathematical	—	`Set.preimage` `Real` `Set` `Set.instMembership` `unitInterval` `Set.Iic` `Real.instPreorder` `Set.Icc` `Set.Elem` `Subtype.preorder` `Set.Icc.instZero` `Real.semiring` `Real.partialOrder` `Real.instIsOrderedRing`	—	`Real.instIsOrderedRing` `Set.preimage_subtype_val_Iic` `ZeroLEOneClass.factZeroLeOne` `Real.instZeroLEOneClass` `Set.Icc_bot`
`subtype_Iio_eq_Ico` 📖	mathematical	—	`Set.preimage` `Real` `Set` `Set.instMembership` `unitInterval` `Set.Iio` `Real.instPreorder` `Set.Ico` `Set.Elem` `Subtype.preorder` `Set.Icc.instZero` `Real.semiring` `Real.partialOrder` `Real.instIsOrderedRing`	—	`Real.instIsOrderedRing` `Set.preimage_subtype_val_Iio` `ZeroLEOneClass.factZeroLeOne` `Real.instZeroLEOneClass` `Set.Ico_bot`
`subtype_Ioi_eq_Ioc` 📖	mathematical	—	`Set.preimage` `Real` `Set` `Set.instMembership` `unitInterval` `Set.Ioi` `Real.instPreorder` `Set.Ioc` `Set.Elem` `Subtype.preorder` `Set.Icc.instOne` `Real.semiring` `Real.partialOrder` `Real.instIsOrderedRing`	—	`Real.instIsOrderedRing` `Set.preimage_subtype_val_Ioi` `ZeroLEOneClass.factZeroLeOne` `Real.instZeroLEOneClass` `Set.Ioc_top`
`symmHomeomorph_apply` 📖	mathematical	—	`DFunLike.coe` `Homeomorph` `Set.Elem` `Real` `unitInterval` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `EquivLike.toFunLike` `Homeomorph.instEquivLike` `symmHomeomorph` `symm`	—	—
`symmHomeomorph_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Homeomorph` `Set.Elem` `Real` `unitInterval` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `EquivLike.toFunLike` `Homeomorph.instEquivLike` `Homeomorph.symm` `symmHomeomorph` `symm`	—	—
`symm_bijective` 📖	mathematical	—	`Function.Bijective` `Set.Elem` `Real` `unitInterval` `symm`	—	`Function.Involutive.bijective` `symm_involutive`
`symm_eq_one` 📖	mathematical	—	`symm` `Set.Elem` `Real` `unitInterval` `Set.Icc.instOne` `Real.semiring` `Real.partialOrder` `Real.instIsOrderedRing` `Set.Icc.instZero`	—	`Real.instIsOrderedRing` `symm_zero`
`symm_eq_zero` 📖	mathematical	—	`symm` `Set.Elem` `Real` `unitInterval` `Set.Icc.instZero` `Real.semiring` `Real.partialOrder` `Real.instIsOrderedRing` `Set.Icc.instOne`	—	`Real.instIsOrderedRing` `symm_one`
`symm_inj` 📖	mathematical	—	`symm`	—	`Function.Bijective.injective` `symm_bijective`
`symm_involutive` 📖	mathematical	—	`Function.Involutive` `Set.Elem` `Real` `unitInterval` `symm`	—	`symm_symm`
`symm_le_comm` 📖	mathematical	—	`Set.Elem` `Real` `unitInterval` `Real.instLE` `Set` `Set.instMembership` `symm`	—	`symm_le_symm` `symm_symm`
`symm_le_symm` 📖	mathematical	—	`Set.Elem` `Real` `unitInterval` `Real.instLE` `Set` `Set.instMembership` `symm`	—	`IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le`
`symm_lt_comm` 📖	mathematical	—	`Set.Elem` `Real` `unitInterval` `Real.instLT` `Set` `Set.instMembership` `symm`	—	`symm_lt_symm` `symm_symm`
`symm_lt_symm` 📖	mathematical	—	`Set.Elem` `Real` `unitInterval` `Real.instLT` `Set` `Set.instMembership` `symm`	—	`IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add`
`symm_one` 📖	mathematical	—	`symm` `Set.Elem` `Real` `unitInterval` `Set.Icc.instOne` `Real.semiring` `Real.partialOrder` `Real.instIsOrderedRing` `Set.Icc.instZero`	—	`Real.instIsOrderedRing` `sub_self`
`symm_projIcc` 📖	mathematical	—	`symm` `Set.projIcc` `Real` `Real.linearOrder` `Real.instZero` `Real.instOne` `zero_le_one` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Real.instZeroLEOneClass` `Real.instSub`	—	`zero_le_one` `Real.instZeroLEOneClass` `le_total` `Real.instIsOrderedRing` `Set.projIcc_of_le_left` `symm_zero` `Set.projIcc_of_right_le` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `CanLift.prf` `Subtype.canLift` `Set.projIcc_val` `symm_one` `AddGroup.toOrderedSub` `covariant_swap_add_of_covariant_add` `zero_add`
`symm_symm` 📖	mathematical	—	`symm`	—	`sub_sub_cancel` `Subtype.coe_eta`
`symm_zero` 📖	mathematical	—	`symm` `Set.Elem` `Real` `unitInterval` `Set.Icc.instZero` `Real.semiring` `Real.partialOrder` `Real.instIsOrderedRing` `Set.Icc.instOne`	—	`Real.instIsOrderedRing` `sub_zero`
`toNNReal_add_toNNReal_symm` 📖	mathematical	—	`NNReal` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `toNNReal` `symm` `instOneNNReal`	—	`NNReal.eq` `add_sub_cancel`
`toNNReal_continuous` 📖	mathematical	—	`Continuous` `Set.Elem` `Real` `unitInterval` `NNReal` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `NNReal.instTopologicalSpace` `toNNReal`	—	`continuous_subtype_val`
`toNNReal_one` 📖	mathematical	—	`toNNReal` `Set.Elem` `Real` `unitInterval` `Set.Icc.instOne` `Real.semiring` `Real.partialOrder` `Real.instIsOrderedRing` `NNReal` `instOneNNReal`	—	`Real.instIsOrderedRing`
`toNNReal_symm_add_toNNReal` 📖	mathematical	—	`NNReal` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `toNNReal` `symm` `instOneNNReal`	—	`NNReal.eq` `sub_add_cancel`
`toNNReal_zero` 📖	mathematical	—	`toNNReal` `Set.Elem` `Real` `unitInterval` `Set.Icc.instZero` `Real.semiring` `Real.partialOrder` `Real.instIsOrderedRing` `NNReal` `instZeroNNReal`	—	`Real.instIsOrderedRing`
`two_mul_sub_one_mem_iff` 📖	mathematical	—	`Real` `Set` `Set.instMembership` `unitInterval` `Real.instSub` `Real.instMul` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Real.instOne` `Set.Icc` `Real.instPreorder` `DivInvMonoid.toDiv` `Real.instDivInvMonoid`	—	`Nat.instAtLeastTwoHAddOfNat` `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.cast_zero` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_zero` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Nat.cast_one` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `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_gt` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Linarith.add_lt_of_le_of_neg` `Real.instIsStrictOrderedRing` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `Real.instIsOrderedRing` `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` `IsStrictOrderedRing.toCharZero` `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` `Mathlib.Meta.NormNum.isNat_lt_true` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Linarith.mul_nonpos` `Mathlib.Meta.NormNum.isNat_add`
`univ_eq_Icc` 📖	mathematical	—	`Set.univ` `Set.Elem` `Real` `unitInterval` `Set.Icc` `Subtype.preorder` `Real.instPreorder` `Set` `Set.instMembership` `Set.Icc.instZero` `Real.semiring` `Real.partialOrder` `Real.instIsOrderedRing` `Set.Icc.instOne`	—	`ZeroLEOneClass.factZeroLeOne` `Real.instZeroLEOneClass` `Set.Icc_bot_top`
`zero_mem` 📖	mathematical	—	`Real` `Set` `Set.instMembership` `unitInterval` `Real.instZero`	—	`le_rfl` `zero_le_one` `Real.instZeroLEOneClass`

---

← Back to Index