liftOrderHom_mk — Mathlib

English

The lifted function respects mk equality: if mk a ha = mk b hb, then f a = f b.

Русский

Поднятая функция сохраняет равенство mk: если mk a ha = mk b hb, то f a = f b.

LaTeX

$$$\text{lift } f h (mk a ha) = f \langle a, ha \rangle$$$

Lean4

@[to_additive (attr := simp)]
theorem liftOrderHom_mk {α : Type*} [PartialOrder α] (f : { a : M // a ≠ 1 } → α)
    (h : ∀ (a b : { a : M // a ≠ 1 }), mk a.val a.prop ≤ mk b.val b.prop → f a ≤ f b) {a : M} (ha : a ≠ 1) :
    liftOrderHom f h (mk a ha) = f ⟨a, ha⟩ :=
  lift_mk f (fun a b heq ↦ le_antisymm (h a b heq.le) (h b a heq.ge)) ha

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