rightRel_apply — Mathlib

English

For all x,y ∈ α, rightRel s x y holds iff y x^{-1} ∈ s.

Русский

Для любых x,y ∈ α, rightRel s x y выполняется тогда и только тогда, когда y x^{-1} ∈ s.

LaTeX

$$rightRel s x y ⇔ y x^{-1} ∈ s$$

Lean4

@[to_additive]
theorem rightRel_apply {x y : α} : rightRel s x y ↔ y * x⁻¹ ∈ s :=
  calc
    (∃ a : s, (a : α) * y = x) ↔ ∃ a : s, y * x⁻¹ = a⁻¹ := by
      simp only [mul_inv_eq_iff_eq_mul, Subgroup.coe_inv, eq_inv_mul_iff_mul_eq]
    _ ↔ y * x⁻¹ ∈ s := by simp [exists_inv_mem_iff_exists_mem]

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