toEquiv_le_toEquiv

Mathlib.Topology.Specialization

URI: https://scilib.ai/kg/mathlib#Specialization.toEquiv_le_toEquiv

English

For any a,b in α, toEquiv a ≤ toEquiv b iff b specializes to a.

Русский

Для любых a,b ∈ α, toEquiv a ≤ toEquiv b эквивалентно тому, что b специализируется на a.

LaTeX

$$$\forall a,b:\; toEquiv(a) \le toEquiv(b) \iff b \triangleright a$$$

Lean4

@[simp]
theorem toEquiv_le_toEquiv {a b : α} : toEquiv a ≤ toEquiv b ↔ b ⤳ a :=
  Iff.rfl

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

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

Разделы

Аффилиация

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