fin_mono

Mathlib.Data.Finset.Fin

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

← MathLib Explorer

English

The operation Finset.fin n is monotone with respect to inclusion: s ⊆ t implies s.fin n ⊆ t.fin n.

Русский

Операция Finset.fin n монотонна по включениям: s ⊆ t ⇒ s.fin n ⊆ t.fin n.

LaTeX

$$s \\subseteq t \\Rightarrow s.fin n \\subseteq t.fin n$$

Lean4

@[mono, deprecated attachFin_subset_attachFin (since := "2025-04-08")]
theorem fin_mono : Monotone (Finset.fin n) := fun s t h x => by simpa using @h x

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

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

Разделы

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

Аффилиация

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