quot_mk_eq_iff — Mathlib

English

Similarly, equivalence between quotients is equivalent to Rel' on the representatives.

Русский

Аналогично, эквивалентность по эквивалентности равна Rel' на представителях.

LaTeX

$$Quot.mk a = Quot.mk b ↔ Rel f g a b$$

Lean4

theorem quot_mk_eq_iff [Mono f] (a b : X₁ ⊕ X₂) : (Quot.mk _ a : Pushout f g) = Quot.mk _ b ↔ Rel' f g a b :=
  by
  rw [← (equivalence_rel' f g).quot_mk_eq_iff]
  exact ⟨fun h => (equivPushout' f g).symm.injective h, fun h => (equivPushout' f g).injective h⟩

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