diff_subset_closure_iff

Mathlib.Topology.Closure

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

English

For sets s,t, s \ t ⊆ closure t iff s ⊆ closure t.

Русский

Для множеств s,t: s \ t ⊆ closure t ⇔ s ⊆ closure t.

LaTeX

$$s \ t \subseteq \overline{t} \iff s \subseteq \overline{t}$$

Lean4

theorem diff_subset_closure_iff : s \ t ⊆ closure t ↔ s ⊆ closure t := by
  rw [diff_subset_iff, union_eq_self_of_subset_left subset_closure]

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

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

Разделы

Аффилиация

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