Documentation Verification Report

Embedding

📁 Source: Mathlib/Data/Real/Embedding.lean

Statistics

Metric	Count
Definitions `embedReal`, `embedRealFun`, `ratLt`, `ratLt'`	4
Theorems `embedRealFun_add`, `embedRealFun_strictMono`, `embedRealFun_zero`, `embedReal_apply`, `embedReal_injective`, `embedReal_one`, `exists_orderAddMonoidHom_real_injective`, `mkRat_mem_ratLt`, `ratLt'_add`, `ratLt'_bddAbove`, `ratLt'_nonempty`, `ratLt_add`, `ratLt_bddAbove`, `ratLt_nonempty`, `mul_smul_one_lt_iff`, `num_le_nat_mul_den`, `num_smul_one_lt_den_smul_add`	17
Total	21

Archimedean

Definitions

Name	Category	Theorems
`embedReal` 📖	CompOp	3 math math: `embedReal_apply`, `embedReal_injective`, `embedReal_one`
`embedRealFun` 📖	CompOp	4 math math: `embedRealFun_add`, `embedReal_apply`, `embedRealFun_zero`, `embedRealFun_strictMono`
`ratLt` 📖	CompOp	4 math math: `ratLt_add`, `ratLt_bddAbove`, `mkRat_mem_ratLt`, `ratLt_nonempty`
`ratLt'` 📖	CompOp	3 math math: `ratLt'_nonempty`, `ratLt'_add`, `ratLt'_bddAbove`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`embedRealFun_add` 📖	mathematical	—	`embedRealFun` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `Real` `Real.instAdd`	—	`embedRealFun.eq_1` `ratLt'_add` `csSup_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `ratLt'_nonempty` `ratLt'_bddAbove`
`embedRealFun_strictMono` 📖	mathematical	—	`StrictMono` `Real` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Real.instPreorder` `embedRealFun`	—	`sub_pos` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `sub_add_cancel` `lt_of_sub_pos` `Real.instIsOrderedAddMonoid` `embedRealFun_add` `add_sub_cancel_right` `arch` `Int.natAbs_of_isUnit` `eq_ratCast` `RingHom.instRingHomClass` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing` `one_smul` `LE.le.trans_lt` `nsmul_lt_nsmul_left` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `Nat.instIsOrderedAddMonoid` `contravariant_lt_of_covariant_le` `Nat.instZeroLEOneClass` `lt_csSup_of_lt` `ratLt'_bddAbove` `Int.instZeroLEOneClass`
`embedRealFun_zero` 📖	mathematical	—	`embedRealFun` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Real` `Real.instZero`	—	`le_antisymm` `csSup_le` `ratLt'_nonempty` `Rat.cast_nonpos` `Real.instIsStrictOrderedRing` `Rat.num_nonpos` `LT.lt.le` `neg_of_smul_neg_right` `SMulPosReflectLE.toSMulPosReflectLT` `SMulPosStrictMono.toSMulPosReflectLE` `instSMulPosStrictMonoIntOfIsOrderedAddMonoid` `zero_le_one` `Set.image_congr` `eq_ratCast` `RingHom.instRingHomClass` `nsmul_zero` `le_csSup_iff` `ratLt'_bddAbove` `mem_upperBounds` `smul_neg_iff_of_neg_left` `IsStrictOrderedRing.toIsOrderedRing` `Int.instIsStrictOrderedRing` `instPosSMulStrictMonoIntOfIsOrderedAddMonoid` `PosSMulMono.toPosSMulReflectLT` `PosSMulStrictMono.toPosSMulMono` `zero_lt_one` `Mathlib.Tactic.Contrapose.contrapose₁` `Mathlib.Tactic.Push.not_forall_eq` `exists_rat_btwn` `Real.instArchimedean`
`embedReal_apply` 📖	mathematical	—	`DFunLike.coe` `OrderAddMonoidHom` `Real` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Real.instPreorder` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Real.instAddMonoid` `OrderAddMonoidHom.instFunLike` `embedReal` `embedRealFun`	—	—
`embedReal_injective` 📖	mathematical	—	`Real` `DFunLike.coe` `OrderAddMonoidHom` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Real.instPreorder` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Real.instAddMonoid` `OrderAddMonoidHom.instFunLike` `embedReal`	—	`StrictMono.injective` `embedRealFun_strictMono`
`embedReal_one` 📖	mathematical	—	`DFunLike.coe` `OrderAddMonoidHom` `Real` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Real.instPreorder` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Real.instAddMonoid` `OrderAddMonoidHom.instFunLike` `embedReal` `Real.instOne`	—	`embedReal_apply` `le_antisymm` `csSup_le` `ratLt'_nonempty` `Nat.cast_one` `mul_one` `one_mul` `LT.lt.le` `smul_lt_smul_iff_of_pos_right` `instSMulPosStrictMonoIntOfIsOrderedAddMonoid` `SMulPosReflectLE.toSMulPosReflectLT` `SMulPosStrictMono.toSMulPosReflectLE` `zero_lt_one` `Real.instIsStrictOrderedRing` `eq_ratCast` `RingHom.instRingHomClass` `natCast_zsmul` `le_csSup_iff` `ratLt'_bddAbove` `Mathlib.Tactic.Contrapose.contrapose₁` `Mathlib.Tactic.Push.not_forall_eq` `exists_rat_btwn` `Real.instArchimedean`
`exists_orderAddMonoidHom_real_injective` 📖	mathematical	—	`Real` `DFunLike.coe` `OrderAddMonoidHom` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Real.instPreorder` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Real.instAddMonoid` `OrderAddMonoidHom.instFunLike`	—	`subsingleton_or_nontrivial` `Function.injective_of_subsingleton` `exists_ne` `abs_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `covariant_swap_add_of_covariant_add` `abs_ne_zero` `embedReal_injective`
`mkRat_mem_ratLt` 📖	mathematical	—	`Set` `Set.instMembership` `ratLt` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddMonoid.toNatSMul` `SubNegMonoid.toAddMonoid`	—	`Set.mem_setOf` `mul_comm` `smul_smul` `natCast_zsmul` `smul_lt_smul_iff_of_pos_left` `instPosSMulStrictMonoNatOfIsOrderedAddMonoid` `PosSMulMono.toPosSMulReflectLT` `instPosSMulMonoNatOfIsOrderedAddMonoid`
`ratLt'_add` 📖	mathematical	—	`ratLt'` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `Set` `Real` `Set.add` `Real.instAdd`	—	`ratLt'.eq_1` `ratLt_add` `Set.image_add` `AddMonoidHomClass.toAddHomClass` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass`
`ratLt'_bddAbove` 📖	mathematical	—	`BddAbove` `Real` `Real.instLE` `ratLt'`	—	`Monotone.map_bddAbove` `Rat.cast_mono` `Real.instIsStrictOrderedRing` `ratLt_bddAbove`
`ratLt'_nonempty` 📖	mathematical	—	`Set.Nonempty` `Real` `ratLt'`	—	`Set.image_nonempty` `ratLt_nonempty`
`ratLt_add` 📖	mathematical	—	`ratLt` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `Set` `Set.add`	—	`Set.ext` `Set.mem_add` `arch` `sub_pos` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Set.mem_setOf_eq` `Mathlib.Tactic.Contrapose.contrapose₃` `zero_nsmul` `mul_ne_zero` `IsStrictOrderedRing.noZeroDivisors` `Nat.instIsStrictOrderedRing` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `Rat.den_ne_zero` `existsUnique_add_zsmul_mem_Ico` `zero_lt_one` `mkRat_mem_ratLt` `smul_smul` `zero_add` `sub_add_cancel` `le_sub_iff_add_le` `Mathlib.Tactic.Abel.subst_into_addg` `Mathlib.Tactic.Abel.term_atomg` `Mathlib.Tactic.Abel.unfold_sub` `Mathlib.Tactic.Abel.subst_into_negg` `Mathlib.Tactic.Abel.term_neg` `neg_zero` `Mathlib.Tactic.Abel.term_add_constg` `Mathlib.Tactic.Abel.term_add_termg` `Mathlib.Meta.NormNum.IsNat.to_eq` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Meta.NormNum.isNat_ofNat` `add_zero` `sub_le_iff_le_add` `smul_add` `smul_sub` `lt_of_lt_of_le` `lt_add_of_pos_left` `LE.le.trans` `sub_smul` `sub_lt_comm` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `natCast_zsmul` `Rat.mkRat_add_mkRat_of_den` `add_sub_cancel` `Rat.mkRat_num_den'` `num_smul_one_lt_den_smul_add`
`ratLt_bddAbove` 📖	mathematical	—	`BddAbove` `ratLt`	—	`arch` `zero_lt_one` `ratLt.eq_1` `mem_upperBounds` `num_le_nat_mul_den` `LT.lt.le` `natCast_zsmul` `Nat.cast_one` `mul_one`
`ratLt_nonempty` 📖	mathematical	—	`Set.Nonempty` `ratLt`	—	`lt_trichotomy` `arch` `zero_lt_one` `neg_lt` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `lt_of_lt_of_le` `add_neg_cancel` `Int.cast_neg` `Int.cast_natCast` `neg_smul` `natCast_zsmul` `one_smul` `Int.cast_one` `nsmul_zero` `Int.natAbs_of_isUnit` `LE.le.trans_lt` `nsmul_lt_nsmul_iff_left` `Nat.instIsOrderedAddMonoid` `contravariant_lt_of_covariant_le` `Nat.instZeroLEOneClass`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mul_smul_one_lt_iff` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddMonoid.toNatSMul` `SubNegMonoid.toAddMonoid`	—	`mul_comm` `SemigroupAction.mul_smul` `natCast_zsmul` `lt_of_smul_lt_smul_left` `PosSMulMono.toPosSMulReflectLT` `PosSMulStrictMono.toPosSMulMono` `instPosSMulStrictMonoIntOfIsOrderedAddMonoid` `zsmul_lt_zsmul_right`
`num_le_nat_mul_den` 📖	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddMonoid.toNatSMul` `SubNegMonoid.toAddMonoid`	—	—	`le_of_smul_le_smul_right` `SMulPosStrictMono.toSMulPosReflectLE` `instSMulPosStrictMonoIntOfIsOrderedAddMonoid` `LE.le.trans` `mul_comm` `smul_smul` `natCast_zsmul` `nsmul_le_nsmul_right` `IsOrderedAddMonoid.toAddLeftMono` `covariant_swap_add_of_covariant_add`
`num_smul_one_lt_den_smul_add` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddMonoid.toNatSMul` `SubNegMonoid.toAddMonoid`	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid`	—	`mul_comm` `mul_smul_one_lt_iff` `Rat.add_num_den'` `smul_smul` `smul_lt_smul_iff_of_pos_left` `instPosSMulStrictMonoIntOfIsOrderedAddMonoid` `PosSMulMono.toPosSMulReflectLT` `PosSMulStrictMono.toPosSMulMono` `add_smul` `smul_add` `add_lt_add` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `mul_pos` `LinearOrderedCommMonoidWithZero.toPosMulStrictMono` `Nat.cast_mul` `mul_assoc` `smul_eq_mul` `smul_assoc` `AddCommGroup.intIsScalarTower`

---

← Back to Index