lift_mk — Mathlib

English

An induction principle for MulArchimedeanClass: to prove a property for all classes, it suffices to prove it for mk a for every a.

Русский

Принцип индукции по MulArchimedeanClass: чтобы доказать свойство для всех классов, достаточно доказать его для mk a для каждого a.

LaTeX

$$$\forall x, P(x) \Leftarrow \forall a, P(mk a)$$$

Lean4

@[to_additive (attr := simp)]
theorem lift_mk {α : Type*} (f : M → α) (h : ∀ a b, mk a = mk b → f a = f b) (a : M) : lift f h (mk a) = f a :=
  by
  unfold lift
  exact Quotient.lift_mk f (fun _ _ h' ↦ h _ _ <| mk_eq_mk.mpr h') a

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