mem_own_rightCoset — Mathlib

English

For a right coset, membership is preserved under right action; in particular, a ∈ s if op a • s = s.

Русский

Для правого косета членство сохраняется при правом действии; в частности, a ∈ s если op a • s = s.

LaTeX

$$mem_rightCoset_rightCoset {a} (ha : op a • (s : Set α) = s) : a ∈ s$$

Lean4

@[to_additive mem_own_rightAddCoset]
theorem mem_own_rightCoset (a : α) : a ∈ op a • (s : Set α) :=
  suffices 1 * a ∈ op a • (s : Set α) by simpa
  mem_rightCoset a (one_mem s : 1 ∈ s)

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