fin_subset_fin

Mathlib.Data.Finset.Fin

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

← MathLib Explorer

English

If s ⊆ t as Finsets, then s.fin n ⊆ t.fin n.

Русский

Если s ⊆ t как Finset, то s.fin n ⊆ t.fin n.

LaTeX

$$Finset.fin n s ⊆ Finset.fin n t$$

Lean4

@[gcongr, deprecated attachFin_subset_attachFin (since := "2025-04-08")]
theorem fin_subset_fin (n : ℕ) {s t : Finset ℕ} (h : s ⊆ t) : s.fin n ⊆ t.fin n :=
  fin_mono h

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

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

Разделы

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

Аффилиация

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