leftRel_apply — Mathlib

English

For all x,y ∈ α, leftRel s x y holds if and only if x⁻¹y ∈ s.

Русский

Для всех x,y ∈ α отношение leftRel s x y выполняется тогда и только тогда, когда x⁻¹y ∈ s.

LaTeX

$$$\text{leftRel}(s)(x,y) \iff x^{-1}y \in s$$$

Lean4

@[to_additive]
theorem leftRel_apply {x y : α} : leftRel s x y ↔ x⁻¹ * y ∈ s :=
  calc
    (∃ a : s.op, y * MulOpposite.unop a = x) ↔ ∃ a : s, y * a = x := s.equivOp.symm.exists_congr_left
    _ ↔ ∃ a : s, x⁻¹ * y = a⁻¹ := by simp only [inv_mul_eq_iff_eq_mul, Subgroup.coe_inv, eq_mul_inv_iff_mul_eq]
    _ ↔ x⁻¹ * y ∈ s := by simp [exists_inv_mem_iff_exists_mem]

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