offDiag_eq_sep_prod

Mathlib.Data.Set.Prod

URI: https://scilib.ai/kg/mathlib#Set.offDiag_eq_sep_prod

English

Let S be a subset of α. Then the off-diagonal of S is the set of all pairs (x,y) in S × S with x ≠ y.

Русский

Пусть S ⊆ α. Тогда множество S.offDiag состоит из всех пар (x, y) ∈ S × S таких, что x ≠ y.

LaTeX

$$$ s.offDiag = \{ (x,y) \in s \times s \mid x \neq y \}$$$

Lean4

theorem offDiag_eq_sep_prod : s.offDiag = {x ∈ s ×ˢ s | x.1 ≠ x.2} :=
  ext fun _ => and_assoc.symm

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru