supIndep'

Mathlib.Order.SupIndep

URI: https://scilib.ai/kg/mathlib#iSupIndep.supIndep'

English

A finite subfamily inherits independence from the whole family.

Русский

Любая конечная подмножество сохраняет независимость из всей семьи.

LaTeX

$$$\\\\forall s: Finset ι,\\\\ iSupIndep f \\\\Rightarrow s.SupIndep f$$$

Lean4

theorem supIndep' {f : ι → α} (s : Finset ι) (h : iSupIndep f) : s.SupIndep f :=
  iSupIndep.supIndep (h.comp Subtype.coe_injective)

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

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

Разделы

Аффилиация

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