coe_offDiag

Mathlib.Data.Finset.Prod

URI: https://scilib.ai/kg/mathlib#Finset.coe_offDiag

English

As sets, the off-diagonal of s coincides with the set of pairs (a,b) with a,b ∈ s and a ≠ b.

Русский

Как множества, вне диагонали s совпадает с множеством пар (a,b), где a,b ∈ s и a ≠ b.

LaTeX

$$$(s\\text{ offDiag}) = \\{(a,b) \\mid a,b \\in s \\land a \\neq b\\}$$$

Lean4

@[simp, norm_cast]
theorem coe_offDiag : (s.offDiag : Set (α × α)) = (s : Set α).offDiag :=
  Set.ext fun _ => mem_offDiag

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

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

Разделы

Аффилиация

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