nhdsKer_minimal

Mathlib.Topology.NhdsKer

URI: https://scilib.ai/kg/mathlib#nhdsKer_minimal

English

If s ⊆ t and t is open, then nhdsKer(s) ⊆ t.

Русский

Если s ⊆ t и t открыто, то nhdsKer(s) ⊆ t.

LaTeX

$$nhdsKer(s) ⊆ t$$

Lean4

theorem nhdsKer_minimal (h₁ : s ⊆ t) (h₂ : IsOpen t) : nhdsKer s ⊆ t := by rw [nhdsKer_def];
  exact sInter_subset_of_mem ⟨h₂, h₁⟩

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

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

Разделы

Аффилиация

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