inseparable_iff_specializes_and

Mathlib.Topology.Inseparable

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

English

Two points are inseparable if and only if they specialize in both directions.

Русский

Два пункта неразделимы тогда и только тогда, когда каждый из них специализируется на другой.

LaTeX

$$$x \\sim_i y \\iff (x \\rightarrow y) \\wedge (y \\rightarrow x).$$$

Lean4

theorem inseparable_iff_specializes_and : (x ~ᵢ y) ↔ x ⤳ y ∧ y ⤳ x :=
  le_antisymm_iff

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

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

Разделы

Аффилиация

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