funUnique — Mathlib

English

The inverse image under the constructed isomorphism of an element a ∈ β equals g(a).

Русский

Образ обратного отображения полученного изоморфизма применённого к элементу a ∈ β равен g(a).

LaTeX

$$$ (\mathrm{ofHomInv}\, f\, g\, h_1\, h_2)^{-1} a = g(a) $$$

Lean4

/-- Order isomorphism between `α → β` and `β`, where `α` has a unique element. -/
@[simps! toEquiv apply]
def funUnique (α β : Type*) [Unique α] [Preorder β] : (α → β) ≃o β
    where
  toEquiv := Equiv.funUnique α β
  map_rel_iff' := by simp [Pi.le_def, Unique.forall_iff]

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