leftCoset_eq_iff — Mathlib

English

Two elements x, y lie in the same left coset of s if and only if x^{-1} y ∈ s.

Русский

Две элементы x, y лежат в одной левой косете подгруппы s тогда и только тогда, когда x^{-1} y ∈ s.

LaTeX

$$$x s = y s \iff x^{-1} y \in s$$$

Lean4

@[to_additive leftAddCoset_eq_iff]
theorem leftCoset_eq_iff {x y : α} : x • (s : Set α) = y • s ↔ x⁻¹ * y ∈ s :=
  by
  rw [Set.ext_iff]
  simp_rw [mem_leftCoset_iff, SetLike.mem_coe]
  constructor
  · intro h
    apply (h y).mpr
    rw [inv_mul_cancel]
    exact s.one_mem
  · intro h z
    rw [← mul_inv_cancel_right x⁻¹ y]
    rw [mul_assoc]
    exact s.mul_mem_cancel_left h

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