mono

Mathlib.Order.SupIndep

URI: https://scilib.ai/kg/mathlib#sSupIndep.mono

English

If t is contained in s and sSupIndep s holds, then sSupIndep t also holds.

Русский

Если t ⊆ s и sSupIndep s, то sSupIndep t также выполняется.

LaTeX

$$sSupIndep s → (t ⊆ s) → sSupIndep t$$

Lean4

theorem mono {t : Set α} (hst : t ⊆ s) : sSupIndep t := fun _ ha =>
  (hs (hst ha)).mono_right (sSup_le_sSup (diff_subset_diff_left hst))

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

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

Разделы

Аффилиация

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