toFinset_offDiag

Mathlib.Data.Finite.Prod

URI: https://scilib.ai/kg/mathlib#Set.Finite.toFinset_offDiag

English

For a finite set s, the toFinset of s.offDiag equals the offDiag of toFinset.

Русский

Для конечного множества s, toFinset(s.offDiag) равен s.toFinset.offDiag.

LaTeX

$$$ hs.offDiag.toFinset = hs.toFinset.offDiag $$$

Lean4

theorem toFinset_offDiag {s : Set α} [DecidableEq α] (hs : s.Finite) : hs.offDiag.toFinset = hs.toFinset.offDiag :=
  Finset.ext <| by simp

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

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

Разделы

Аффилиация

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