lift_eq_iff — Mathlib

English

The two-labeled equality for pairs in M × S is equivalent to equality after applying g to the prod.

Русский

Две пары в M × S эквивалентны по равенству после приложения g к произведению.

LaTeX

$$$ f.lift hg (f.mk' x.1 x.2) = f.lift hg (f.mk' y.1 y.2) \iff g(x.1 \cdot y.2) = g(y.1 \cdot x.2) $$$

Lean4

@[to_additive]
theorem lift_eq_iff {x y : M × S} :
    f.lift hg (f.mk' x.1 x.2) = f.lift hg (f.mk' y.1 y.2) ↔ g (x.1 * y.2) = g (y.1 * x.2) := by
  rw [lift_mk', lift_mk', mul_inv hg]

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