lift_mk — Mathlib

English

The lifting is compatible with equivalence of representatives, i.e., mk a ha and mk b hb are identified when their mk are equal.

Русский

lifting согласуется с эквивалентностью представителей: mk a ha = mk b hb тогда и только тогда, когда соответствующие mk эквивалентны.

LaTeX

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

Lean4

@[to_additive (attr := simp)]
theorem lift_mk {α : Type*} (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) :
    lift f h (mk a ha) = f ⟨a, ha⟩ := by simp [lift, mk, ha]

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