lift_ι_apply — Mathlib

English

A defining property that expresses that lift is the unique representative of a given action on ι_R.

Русский

Свойство, выражающее, что lift является единственным представителем для заданного действия на ι_R.

LaTeX

$$$\text{liftUnique}(f,g): (g\circ ι_R = f) \iff g = lift_R f$$$

Lean4

@[simp]
theorem lift_ι_apply (f : X → A) (x) : lift R f (ι R x) = f x :=
  by
  rw [ι_def, lift]
  rfl

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