subset_compl_right

Mathlib.Topology.MetricSpace.MetricSeparated

URI: https://scilib.ai/kg/mathlib#Metric.AreSeparated.subset_compl_right

English

If s is ε-separated from t, then s ⊆ tᶜ.

Русский

Если s ε-разделено от t, то s ⊆ tᶜ.

LaTeX

$$$\\operatorname{subset\\_compl\\_right}(h) : s \\subseteq t^{\\complement}$$$

Lean4

theorem subset_compl_right (h : AreSeparated s t) : s ⊆ tᶜ := fun _ hs ht => h.disjoint.le_bot ⟨hs, ht⟩

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

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

Разделы

Аффилиация

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