dirSupInaccOn

Mathlib.Topology.Order.ScottTopology

URI: https://scilib.ai/kg/mathlib#DirSupInacc.dirSupInaccOn

English

If D1 ⊆ D2 and DirSupInaccOn D2 s holds, then DirSupInaccOn D1 s also holds.

Русский

Если D1 ⊆ D2 и DirSupInaccOn D2 s выполняется, то DirSupInaccOn D1 s тоже выполняется.

LaTeX

$$$\\forall \\{D_1,D_2\\}\\ (D_1\\subseteq D_2)\\to DirSupInaccOn(D_2,s)\\to DirSupInaccOn(D_1,s)$$

Lean4

@[simp]
theorem dirSupInaccOn {D : Set (Set α)} : DirSupInacc s → DirSupInaccOn D s := fun h _ _ d₂ d₃ _ hda => h d₂ d₃ hda

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

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

Разделы

Аффилиация

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