toFinset_nontrivial

Mathlib.Data.Fintype.Sets

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

English

s is nontrivial iff s.toFinset is nontrivial.

Русский

Общее множество не тривиально тогда и только тогда, когда его toFinset не тривиальна.

LaTeX

$$$s.toFinset.Nontrivial \iff s.Nontrivial$$$

Lean4

@[simp]
theorem toFinset_nontrivial [Fintype s] : s.toFinset.Nontrivial ↔ s.Nontrivial := by
  rw [Finset.Nontrivial, coe_toFinset]

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

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

Разделы

Аффилиация

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