Pulling back linearly ordered fields along injective maps #
@[reducible, inline]
abbrev
Function.Injective.linearOrderedSemifield
{α : Type u_1}
{β : Type u_2}
[Zero β]
[One β]
[Add β]
[Mul β]
[Pow β ℕ]
[SMul ℕ β]
[SMul ℚ≥0 β]
[NatCast β]
[NNRatCast β]
[Inv β]
[Div β]
[Pow β ℤ]
[Sup β]
[Inf β]
(f : β → α)
(hf : Function.Injective f)
[LinearOrderedSemifield α]
(zero : f 0 = 0)
(one : f 1 = 1)
(add : ∀ (x y : β), f (x + y) = f x + f y)
(mul : ∀ (x y : β), f (x * y) = f x * f y)
(inv : ∀ (x : β), f x⁻¹ = (f x)⁻¹)
(div : ∀ (x y : β), f (x / y) = f x / f y)
(nsmul : ∀ (n : ℕ) (x : β), f (n • x) = n • f x)
(nnqsmul : ∀ (q : ℚ≥0) (x : β), f (q • x) = q • f x)
(npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n)
(zpow : ∀ (x : β) (n : ℤ), f (x ^ n) = f x ^ n)
(natCast : ∀ (n : ℕ), f ↑n = ↑n)
(nnratCast : ∀ (q : ℚ≥0), f ↑q = ↑q)
(hsup : ∀ (x y : β), f (x ⊔ y) = max (f x) (f y))
(hinf : ∀ (x y : β), f (x ⊓ y) = min (f x) (f y))
:
Pullback a LinearOrderedSemifield under an injective map.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[reducible, inline]
abbrev
Function.Injective.linearOrderedField
{α : Type u_1}
{β : Type u_2}
[Zero β]
[One β]
[Add β]
[Mul β]
[Neg β]
[Sub β]
[Pow β ℕ]
[SMul ℕ β]
[SMul ℤ β]
[SMul ℚ≥0 β]
[SMul ℚ β]
[NatCast β]
[IntCast β]
[NNRatCast β]
[RatCast β]
[Inv β]
[Div β]
[Pow β ℤ]
[Sup β]
[Inf β]
(f : β → α)
(hf : Function.Injective f)
[LinearOrderedField α]
(zero : f 0 = 0)
(one : f 1 = 1)
(add : ∀ (x y : β), f (x + y) = f x + f y)
(mul : ∀ (x y : β), f (x * y) = f x * f y)
(neg : ∀ (x : β), f (-x) = -f x)
(sub : ∀ (x y : β), f (x - y) = f x - f y)
(inv : ∀ (x : β), f x⁻¹ = (f x)⁻¹)
(div : ∀ (x y : β), f (x / y) = f x / f y)
(nsmul : ∀ (n : ℕ) (x : β), f (n • x) = n • f x)
(zsmul : ∀ (n : ℤ) (x : β), f (n • x) = n • f x)
(nnqsmul : ∀ (q : ℚ≥0) (x : β), f (q • x) = q • f x)
(qsmul : ∀ (q : ℚ) (x : β), f (q • x) = q • f x)
(npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n)
(zpow : ∀ (x : β) (n : ℤ), f (x ^ n) = f x ^ n)
(natCast : ∀ (n : ℕ), f ↑n = ↑n)
(intCast : ∀ (n : ℤ), f ↑n = ↑n)
(nnratCast : ∀ (q : ℚ≥0), f ↑q = ↑q)
(ratCast : ∀ (q : ℚ), f ↑q = ↑q)
(hsup : ∀ (x y : β), f (x ⊔ y) = max (f x) (f y))
(hinf : ∀ (x y : β), f (x ⊓ y) = min (f x) (f y))
:
Pullback a LinearOrderedField under an injective map.
Equations
- One or more equations did not get rendered due to their size.