CompleteField

📁 Source: Mathlib/Algebra/Order/CompleteField.lean

Statistics

Metric	Count
Definitions `ConditionallyCompleteLinearOrderedField`, `inducedAddHom`, `inducedMap`, `inducedOrderRingHom`, `inducedOrderRingIso`, `toConditionallyCompleteLinearOrder`, `toField`, `uniqueOrderRingHom`, `uniqueOrderRingIso`, `cutMap`, `inducedAddHom`, `inducedMap`, `inducedOrderRingHom`, `inducedOrderRingIso`	14
Theorems `coe_inducedOrderRingIso`, `coe_lt_inducedMap_iff`, `exists_mem_cutMap_mul_self_of_lt_inducedMap_mul_self`, `inducedMap_add`, `inducedMap_inducedMap`, `inducedMap_inv_self`, `inducedMap_mono`, `inducedMap_nonneg`, `inducedMap_one`, `inducedMap_rat`, `inducedMap_self`, `inducedMap_zero`, `inducedOrderRingHom_toFun`, `inducedOrderRingIso_self`, `inducedOrderRingIso_symm`, `le_inducedMap_mul_self_of_mem_cutMap`, `lt_inducedMap_iff`, `toIsOrderedCancelAddMonoid`, `toIsStrictOrderedRing`, `toMulPosStrictMono`, `toPosMulStrictMono`, `toZeroLEOneClass`, `to_archimedean`, `coe_inducedOrderRingIso`, `coe_lt_inducedMap_iff`, `coe_mem_cutMap_iff`, `cutMap_add`, `cutMap_bddAbove`, `cutMap_coe`, `cutMap_mono`, `cutMap_nonempty`, `cutMap_self`, `exists_mem_cutMap_mul_self_of_lt_inducedMap_mul_self`, `inducedMap_add`, `inducedMap_inducedMap`, `inducedMap_inv_self`, `inducedMap_mono`, `inducedMap_nonneg`, `inducedMap_one`, `inducedMap_rat`, `inducedMap_self`, `inducedMap_zero`, `inducedOrderRingIso_self`, `inducedOrderRingIso_symm`, `le_inducedMap_mul_self_of_mem_cutMap`, `lt_inducedMap_iff`, `mem_cutMap_iff`	47
Total	61

ConditionallyCompleteLinearOrderedField

Definitions

Name	Category	Theorems
`inducedAddHom` 📖	CompOp	1 math math: `inducedOrderRingHom_toFun`
`inducedMap` 📖	CompOp	26 math math: `inducedMap_mono`, `LinearOrderedField.lt_inducedMap_iff`, `inducedMap_inv_self`, `inducedMap_rat`, `coe_inducedOrderRingIso`, `inducedMap_one`, `LinearOrderedField.le_inducedMap_mul_self_of_mem_cutMap`, `coe_lt_inducedMap_iff`, `LinearOrderedField.inducedMap_one`, `LinearOrderedField.inducedMap_add`, `LinearOrderedField.inducedMap_mono`, `LinearOrderedField.inducedMap_inv_self`, `LinearOrderedField.inducedMap_zero`, `inducedMap_inducedMap`, `LinearOrderedField.inducedMap_nonneg`, `LinearOrderedField.coe_inducedOrderRingIso`, `LinearOrderedField.coe_lt_inducedMap_iff`, `inducedMap_zero`, `LinearOrderedField.inducedMap_self`, `inducedMap_nonneg`, `inducedMap_add`, `LinearOrderedField.inducedMap_inducedMap`, `le_inducedMap_mul_self_of_mem_cutMap`, `inducedMap_self`, `LinearOrderedField.inducedMap_rat`, `lt_inducedMap_iff`
`inducedOrderRingHom` 📖	CompOp	1 math math: `inducedOrderRingHom_toFun`
`inducedOrderRingIso` 📖	CompOp	6 math math: `inducedOrderRingIso_symm`, `LinearOrderedField.inducedOrderRingIso_self`, `coe_inducedOrderRingIso`, `LinearOrderedField.inducedOrderRingIso_symm`, `LinearOrderedField.coe_inducedOrderRingIso`, `inducedOrderRingIso_self`
`toConditionallyCompleteLinearOrder` 📖	CompOp	5 math math: `toZeroLEOneClass`, `toPosMulStrictMono`, `toIsOrderedCancelAddMonoid`, `toIsStrictOrderedRing`, `toMulPosStrictMono`
`toField` 📖	CompOp	5 math math: `toZeroLEOneClass`, `toPosMulStrictMono`, `toIsOrderedCancelAddMonoid`, `toIsStrictOrderedRing`, `toMulPosStrictMono`
`uniqueOrderRingHom` 📖	CompOp	—
`uniqueOrderRingIso` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_inducedOrderRingIso` 📖	mathematical	—	`DFunLike.coe` `OrderRingIso` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `Distrib.toAdd` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `EquivLike.toFunLike` `OrderRingIso.instEquivLike` `inducedOrderRingIso` `inducedMap` `ConditionallyCompleteLinearOrder.toLinearOrder`	—	—
`coe_lt_inducedMap_iff` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `DivisionRing.toRatCast` `Field.toDivisionRing` `inducedMap` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`Monotone.reflect_lt` `inducedMap_mono` `inducedMap_rat` `exists_rat_btwn` `lt_csSup_of_lt` `LinearOrderedField.cutMap_bddAbove` `LinearOrderedField.coe_mem_cutMap_iff` `IsStrictOrderedRing.toCharZero`
`exists_mem_cutMap_mul_self_of_lt_inducedMap_mul_self` 📖	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` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `inducedMap`	`Set` `Set.instMembership` `LinearOrderedField.cutMap` `Field.toDivisionRing` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `Preorder.toLT` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	—	`lt_or_ge` `Rat.cast_zero` `LinearOrderedField.coe_mem_cutMap_iff` `IsStrictOrderedRing.toCharZero` `mul_self_pos` `AddGroup.existsAddOfLE` `IsStrictOrderedRing.toPosMulStrictMono` `IsStrictOrderedRing.toMulPosStrictMono` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `contravariant_lt_of_covariant_le` `LT.lt.ne'` `exists_rat_pow_btwn` `to_archimedean` `two_ne_zero` `LE.le.trans_lt` `pow_two` `Rat.cast_mul` `lt_inducedMap_iff` `lt_of_mul_self_lt_mul_self₀` `IsOrderedRing.toMulPosMono` `inducedMap_nonneg` `LT.lt.le` `mul_self_lt_mul_self` `Nat.cast_zero` `LT.lt.trans'` `Rat.cast_pow`
`inducedMap_add` 📖	mathematical	—	`inducedMap` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing`	—	`inducedMap.eq_1` `LinearOrderedField.cutMap_add` `csSup_add` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `covariant_swap_add_of_covariant_add` `LinearOrderedField.cutMap_nonempty` `LinearOrderedField.cutMap_bddAbove`
`inducedMap_inducedMap` 📖	mathematical	—	`inducedMap` `ConditionallyCompleteLinearOrder.toLinearOrder`	—	`eq_of_forall_rat_lt_iff_lt` `to_archimedean` `coe_lt_inducedMap_iff`
`inducedMap_inv_self` 📖	mathematical	—	`inducedMap` `ConditionallyCompleteLinearOrder.toLinearOrder`	—	`inducedMap_inducedMap` `to_archimedean` `inducedMap_self`
`inducedMap_mono` 📖	mathematical	—	`Monotone` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `inducedMap`	—	`csSup_le_csSup` `LinearOrderedField.cutMap_bddAbove` `LinearOrderedField.cutMap_nonempty` `LinearOrderedField.cutMap_mono`
`inducedMap_nonneg` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing`	`Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `inducedMap`	—	`LE.le.trans` `Eq.ge` `inducedMap_zero` `inducedMap_mono`
`inducedMap_one` 📖	mathematical	—	`inducedMap` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing`	—	`Nat.cast_one` `Rat.cast_one` `inducedMap_rat`
`inducedMap_rat` 📖	mathematical	—	`inducedMap` `DivisionRing.toRatCast` `Field.toDivisionRing`	—	`csSup_eq_of_forall_le_of_forall_lt_exists_gt` `LinearOrderedField.cutMap_nonempty` `LinearOrderedField.cutMap_coe` `le_of_lt` `exists_rat_btwn` `to_archimedean`
`inducedMap_self` 📖	mathematical	—	`inducedMap` `ConditionallyCompleteLinearOrder.toLinearOrder`	—	`eq_of_forall_rat_lt_iff_lt` `to_archimedean` `coe_lt_inducedMap_iff`
`inducedMap_zero` 📖	mathematical	—	`inducedMap` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing`	—	`Nat.cast_zero` `Rat.cast_zero` `inducedMap_rat`
`inducedOrderRingHom_toFun` 📖	mathematical	—	`DFunLike.coe` `OrderRingHom` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `OrderRingHom.instFunLike` `inducedOrderRingHom` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `Field.toCommRing` `AddMonoidHom.instFunLike` `inducedAddHom`	—	—
`inducedOrderRingIso_self` 📖	mathematical	—	`inducedOrderRingIso` `OrderRingIso.refl` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `Distrib.toAdd` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	—	`OrderRingIso.ext` `inducedMap_self`
`inducedOrderRingIso_symm` 📖	mathematical	—	`OrderRingIso.symm` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `Distrib.toAdd` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `inducedOrderRingIso`	—	—
`le_inducedMap_mul_self_of_mem_cutMap` 📖	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` `Set.instMembership` `LinearOrderedField.cutMap` `Field.toDivisionRing` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	`Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `inducedMap`	—	`exists_rat_pow_btwn` `two_ne_zero` `mul_self_pos` `AddGroup.existsAddOfLE` `IsStrictOrderedRing.toPosMulStrictMono` `IsStrictOrderedRing.toMulPosStrictMono` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `contravariant_lt_of_covariant_le` `LT.lt.ne'` `LT.lt.le` `pow_two` `mul_self_le_mul_self` `IsOrderedRing.toPosMulMono` `IsOrderedRing.toMulPosMono` `Nat.cast_zero` `le_csSup` `LinearOrderedField.cutMap_bddAbove` `LinearOrderedField.coe_mem_cutMap_iff` `IsStrictOrderedRing.toCharZero` `lt_of_mul_self_lt_mul_self₀`
`lt_inducedMap_iff` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `inducedMap` `DivisionRing.toRatCast` `Field.toDivisionRing` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`coe_lt_inducedMap_iff` `exists_rat_btwn` `to_archimedean` `LT.lt.trans`
`toIsOrderedCancelAddMonoid` 📖	mathematical	—	`IsOrderedCancelAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `CommRing.toRing` `Field.toCommRing` `toField` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `toConditionallyCompleteLinearOrder`	—	—
`toIsStrictOrderedRing` 📖	mathematical	—	`IsStrictOrderedRing` `Ring.toSemiring` `CommRing.toRing` `Field.toCommRing` `toField` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `toConditionallyCompleteLinearOrder`	—	`toIsOrderedCancelAddMonoid` `toZeroLEOneClass` `Field.toNontrivial` `toPosMulStrictMono` `toMulPosStrictMono`
`toMulPosStrictMono` 📖	mathematical	—	`MulPosStrictMono` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `CommRing.toRing` `Field.toCommRing` `toField` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `toConditionallyCompleteLinearOrder`	—	—
`toPosMulStrictMono` 📖	mathematical	—	`PosMulStrictMono` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `CommRing.toRing` `Field.toCommRing` `toField` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `toConditionallyCompleteLinearOrder`	—	—
`toZeroLEOneClass` 📖	mathematical	—	`ZeroLEOneClass` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `CommRing.toRing` `Field.toCommRing` `toField` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `toConditionallyCompleteLinearOrder`	—	—
`to_archimedean` 📖	mathematical	—	`Archimedean` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	—	`archimedean_iff_nat_lt` `Mathlib.Tactic.Push.not_forall_eq` `csSup_le` `Set.range_nonempty` `Set.forall_mem_range` `le_sub_iff_add_le` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `le_csSup` `Nat.cast_succ` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `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.sub_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `neg_neg_of_pos` `Mathlib.Tactic.Linarith.zero_lt_one` `Mathlib.Tactic.Linarith.sub_nonpos_of_le`

LinearOrderedField

Definitions

Name	Category	Theorems
`cutMap` 📖	CompOp	10 math math: `cutMap_add`, `cutMap_coe`, `cutMap_nonempty`, `exists_mem_cutMap_mul_self_of_lt_inducedMap_mul_self`, `coe_mem_cutMap_iff`, `cutMap_self`, `cutMap_bddAbove`, `cutMap_mono`, `mem_cutMap_iff`, `ConditionallyCompleteLinearOrderedField.exists_mem_cutMap_mul_self_of_lt_inducedMap_mul_self`
`inducedAddHom` 📖	CompOp	—
`inducedMap` 📖	CompOp	—
`inducedOrderRingHom` 📖	CompOp	—
`inducedOrderRingIso` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_inducedOrderRingIso` 📖	mathematical	—	`DFunLike.coe` `OrderRingIso` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `Distrib.toAdd` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `EquivLike.toFunLike` `OrderRingIso.instEquivLike` `ConditionallyCompleteLinearOrderedField.inducedOrderRingIso` `ConditionallyCompleteLinearOrderedField.inducedMap` `ConditionallyCompleteLinearOrder.toLinearOrder`	—	`ConditionallyCompleteLinearOrderedField.coe_inducedOrderRingIso`
`coe_lt_inducedMap_iff` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `DivisionRing.toRatCast` `Field.toDivisionRing` `ConditionallyCompleteLinearOrderedField.inducedMap` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`ConditionallyCompleteLinearOrderedField.coe_lt_inducedMap_iff`
`coe_mem_cutMap_iff` 📖	mathematical	—	`Set` `Set.instMembership` `cutMap` `DivisionRing.toRatCast` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Field.toDivisionRing`	—	`Function.Injective.mem_set_image` `Rat.cast_injective`
`cutMap_add` 📖	mathematical	—	`cutMap` `Field.toDivisionRing` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `Set` `Set.add`	—	`HasSubset.Subset.antisymm` `Set.instAntisymmSubset` `Set.image_subset_iff` `exists_rat_btwn` `sub_lt_iff_lt_add` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `instIsRightCancelAddOfAddRightReflectLE` `contravariant_swap_add_of_contravariant_add` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `contravariant_lt_of_covariant_le` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `covariant_swap_add_of_covariant_add` `Set.mem_setOf_eq` `coe_mem_cutMap_iff` `IsStrictOrderedRing.toCharZero` `sub_lt_comm` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `add_sub_cancel` `Rat.cast_add` `add_lt_add`
`cutMap_bddAbove` 📖	mathematical	—	`BddAbove` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `cutMap` `Field.toDivisionRing`	—	`exists_rat_gt` `Set.forall_mem_image` `LT.lt.le` `LT.lt.trans'`
`cutMap_coe` 📖	mathematical	—	`cutMap` `Field.toDivisionRing` `DivisionRing.toRatCast` `Set.image` `setOf` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	—
`cutMap_mono` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Set` `Set.instHasSubset` `cutMap`	—	`Set.image_mono` `LE.le.trans_lt'`
`cutMap_nonempty` 📖	mathematical	—	`Set.Nonempty` `cutMap` `Field.toDivisionRing`	—	`Set.Nonempty.image` `exists_rat_lt`
`cutMap_self` 📖	mathematical	—	`cutMap` `Field.toDivisionRing` `Set` `Set.instInter` `Set.Iio` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set.range` `DivisionRing.toRatCast`	—	—
`exists_mem_cutMap_mul_self_of_lt_inducedMap_mul_self` 📖	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` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `ConditionallyCompleteLinearOrderedField.inducedMap`	`Set` `Set.instMembership` `cutMap` `Field.toDivisionRing` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `Preorder.toLT` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	—	`ConditionallyCompleteLinearOrderedField.exists_mem_cutMap_mul_self_of_lt_inducedMap_mul_self`
`inducedMap_add` 📖	mathematical	—	`ConditionallyCompleteLinearOrderedField.inducedMap` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing`	—	`ConditionallyCompleteLinearOrderedField.inducedMap_add`
`inducedMap_inducedMap` 📖	mathematical	—	`ConditionallyCompleteLinearOrderedField.inducedMap` `ConditionallyCompleteLinearOrder.toLinearOrder`	—	`ConditionallyCompleteLinearOrderedField.inducedMap_inducedMap`
`inducedMap_inv_self` 📖	mathematical	—	`ConditionallyCompleteLinearOrderedField.inducedMap` `ConditionallyCompleteLinearOrder.toLinearOrder`	—	`ConditionallyCompleteLinearOrderedField.inducedMap_inv_self`
`inducedMap_mono` 📖	mathematical	—	`Monotone` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderedField.inducedMap`	—	`ConditionallyCompleteLinearOrderedField.inducedMap_mono`
`inducedMap_nonneg` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing`	`Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `ConditionallyCompleteLinearOrderedField.inducedMap`	—	`ConditionallyCompleteLinearOrderedField.inducedMap_nonneg`
`inducedMap_one` 📖	mathematical	—	`ConditionallyCompleteLinearOrderedField.inducedMap` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing`	—	`ConditionallyCompleteLinearOrderedField.inducedMap_one`
`inducedMap_rat` 📖	mathematical	—	`ConditionallyCompleteLinearOrderedField.inducedMap` `DivisionRing.toRatCast` `Field.toDivisionRing`	—	`ConditionallyCompleteLinearOrderedField.inducedMap_rat`
`inducedMap_self` 📖	mathematical	—	`ConditionallyCompleteLinearOrderedField.inducedMap` `ConditionallyCompleteLinearOrder.toLinearOrder`	—	`ConditionallyCompleteLinearOrderedField.inducedMap_self`
`inducedMap_zero` 📖	mathematical	—	`ConditionallyCompleteLinearOrderedField.inducedMap` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing`	—	`ConditionallyCompleteLinearOrderedField.inducedMap_zero`
`inducedOrderRingIso_self` 📖	mathematical	—	`ConditionallyCompleteLinearOrderedField.inducedOrderRingIso` `OrderRingIso.refl` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `Distrib.toAdd` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	—	`ConditionallyCompleteLinearOrderedField.inducedOrderRingIso_self`
`inducedOrderRingIso_symm` 📖	mathematical	—	`OrderRingIso.symm` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `Distrib.toAdd` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderedField.inducedOrderRingIso`	—	`ConditionallyCompleteLinearOrderedField.inducedOrderRingIso_symm`
`le_inducedMap_mul_self_of_mem_cutMap` 📖	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` `Set.instMembership` `cutMap` `Field.toDivisionRing` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	`Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `ConditionallyCompleteLinearOrderedField.inducedMap`	—	`ConditionallyCompleteLinearOrderedField.le_inducedMap_mul_self_of_mem_cutMap`
`lt_inducedMap_iff` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderedField.inducedMap` `DivisionRing.toRatCast` `Field.toDivisionRing` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`ConditionallyCompleteLinearOrderedField.lt_inducedMap_iff`
`mem_cutMap_iff` 📖	mathematical	—	`Set` `Set.instMembership` `cutMap` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `DivisionRing.toRatCast` `Field.toDivisionRing`	—	—

(root)

Definitions

Name	Category	Theorems
`ConditionallyCompleteLinearOrderedField` 📖	CompData	—

---

← Back to Index