toOrderMonoidIso — Mathlib

English

If x ≠ 1, then f x > 0.

Русский

Если x ≠ 1, то f x > 0.

LaTeX

$$$x \neq 1 \Rightarrow 0 < f(x)$$$

Lean4

/-- Turn an element of a type `F` satisfying `OrderIsoClass F α β` and `MulEquivClass F α β`
into an actual `OrderMonoidIso`. This is declared as the default coercion from `F` to `α ≃*o β`. -/
@[to_additive (attr := coe) /-- Turn an element of a type `F` satisfying `OrderIsoClass F α β` and `AddEquivClass F α β`
      into an actual `OrderAddMonoidIso`.
      This is declared as the default coercion from `F` to `α ≃+o β`. -/
    ]
def toOrderMonoidIso [EquivLike F α β] [OrderIsoClass F α β] [MulEquivClass F α β] (f : F) : α ≃*o β :=
  { (f : α ≃* β) with map_le_map_iff' := OrderIsoClass.map_le_map_iff f }

Похожие утверждения