nhdsKer_subset

Mathlib.Topology.NhdsKer

URI: https://scilib.ai/kg/mathlib#IsOpen.nhdsKer_subset

English

For open t, nhdsKer(s) ⊆ t iff s ⊆ t.

Русский

Для открытого t верно: nhdsKer(s) ⊆ t эквивалентно s ⊆ t.

LaTeX

$$IsOpen(t) ⇒ (nhdsKer(s) ⊆ t ↔ s ⊆ t)$$

Lean4

theorem nhdsKer_subset (ht : IsOpen t) : nhdsKer s ⊆ t ↔ s ⊆ t :=
  ⟨subset_nhdsKer.trans, fun h ↦ nhdsKer_minimal h ht⟩

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

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

Разделы

Аффилиация

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