mono

Mathlib.Topology.Order.ScottTopology

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

English

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

Русский

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

LaTeX

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

Lean4

theorem mono {D₁ D₂ : Set (Set α)} (hD : D₁ ⊆ D₂) (hf : DirSupInaccOn D₂ s) : DirSupInaccOn D₁ s := fun ⦃_⦄ a ↦
  hf (hD a)

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

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

Разделы

Аффилиация

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