toFinset_ssubset_toFinset

Mathlib.Data.Fintype.Sets

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

← MathLib Explorer

English

Equality of s.toFinset ⊂ t.toFinset with s ⊂ t for finite s.

Русский

Эквивалентность s.toFinset ⊂ t.toFinset и s ⊂ t для конечного s.

LaTeX

$$$\forall s,t:\ Set α,\ s.toFinset \subset t.toFinset \iff s \subset t$$$

Lean4

@[mono]
theorem toFinset_ssubset_toFinset [Fintype s] [Fintype t] : s.toFinset ⊂ t.toFinset ↔ s ⊂ t := by
  simp only [Finset.ssubset_def, toFinset_subset_toFinset, ssubset_def]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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