one_mem_div_iff — Mathlib

English

Let α be a group and s, t be subsets of α. Then 1 lies in the pointwise division s / t if and only if s and t have a nonempty intersection.

Русский

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

LaTeX

$$$ (1 : \alpha) \in s / t \iff s \cap t \neq \emptyset $$$

Lean4

@[to_additive (attr := simp)]
theorem one_mem_div_iff : (1 : α) ∈ s / t ↔ ¬Disjoint s t := by
  simp [not_disjoint_iff_nonempty_inter, mem_div, div_eq_one, Set.Nonempty]

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