bot_rel_eq_leftRel — Mathlib

English

bot_rel_eq_leftRel: the left relation induced by the bottom subgroup ⊥ coincides with the left quotient relation by H.

Русский

bot_rel_eq_leftRel: левая связь, индуцированная подгруппой ⊥, совпадает с левой факторной связью по H.

LaTeX

$$$ (setoid \\uparrow(⊥) \\uparrow H).r = (QuotientGroup.leftRel H).r $$$

Lean4

theorem bot_rel_eq_leftRel (H : Subgroup G) : ⇑(setoid ↑(⊥ : Subgroup G) ↑H) = ⇑(QuotientGroup.leftRel H) :=
  by
  ext a b
  rw [rel_iff, QuotientGroup.leftRel_apply]
  constructor
  · rintro ⟨a, rfl : a = 1, b, hb, rfl⟩
    rwa [one_mul, inv_mul_cancel_left]
  · rintro (h : a⁻¹ * b ∈ H)
    exact ⟨1, rfl, a⁻¹ * b, h, by rw [one_mul, mul_inv_cancel_left]⟩

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