closure_le

Mathlib.Topology.Sets.Closeds

URI: https://scilib.ai/kg/mathlib#TopologicalSpace.Closeds.closure_le

English

For any closed subset t, closure s ≤ t is equivalent to s ⊆ t.

Русский

Для любого замкнутого подмножества t равенство closure s ≤ t эквивалентно s ⊆ t.

LaTeX

$$$.closure s ≤ t \iff s \subseteq t$$

Lean4

@[simp]
theorem closure_le {s : Set α} {t : Closeds α} : .closure s ≤ t ↔ s ⊆ t :=
  t.isClosed.closure_subset_iff

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

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

Разделы

Аффилиация

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