one_mem_inv_mul_iff — Mathlib

English

Let α be a group and s, t subsets of α. Then 1 belongs to t^{-1} s if and only if s and t intersect nontrivially.

Русский

Пусть α — группа, и s, t — подмножества α. Тогда 1 принадлежит t^{-1} s тогда и только тогда, когда s и t пересекаются ненулево.

LaTeX

$$$ 1 \in t^{-1} s \iff s \cap t \neq \emptyset $$$

Lean4

@[to_additive (attr := simp)]
theorem one_mem_inv_mul_iff : (1 : α) ∈ t⁻¹ * s ↔ ¬Disjoint s t := by
  aesop (add simp [not_disjoint_iff_nonempty_inter, mem_mul, mul_eq_one_iff_eq_inv, Set.Nonempty])

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