subset

Mathlib.Order.SupIndep

URI: https://scilib.ai/kg/mathlib#Finset.SupIndep.subset

English

If t is SupIndep f and h is a subset relation, then s ⊆ t implies s.SupIndep f.

Русский

Если t SupIndep f и s ⊆ t, то s SupIndep f.

LaTeX

$$$\\text{SupIndep}(t,f) \\land s \\subseteq t \\Rightarrow \\text{SupIndep}(s,f).$$$

Lean4

theorem subset (ht : t.SupIndep f) (h : s ⊆ t) : s.SupIndep f := fun _ hu _ hi => ht (hu.trans h) (h hi)

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

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

Разделы

Аффилиация

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