coe_ofMapLEIff — Mathlib

English

If hf provides a function f: α → β and a proof that f(a) ≤ f(b) ↔ a ≤ b for all a,b, then the embedding produced by ofMapLEIff has underlying function f.

Русский

Организация отображения: если дано отображение f: α → β и доказано, что f(a) ≤ f(b) ↔ a ≤ b, то полученное вложение имеет основанную функцию f.

LaTeX

$$$\forall a\in\alpha:\ (\text{ofMapLEIff}(f,h))\,a = f(a)$$$

Lean4

@[simp]
theorem coe_ofMapLEIff {α β} [PartialOrder α] [Preorder β] {f : α → β} (h) : ⇑(ofMapLEIff f h) = f :=
  rfl

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