ofEquiv_specializes_ofEquiv

Mathlib.Topology.Specialization

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

English

For any a,b in the specialization, the specialization a ⤳ b is equivalent to b ≤ a in the preorder.

Русский

Для любых a,b в специализации, a ⤳ b эквивалентно b ≤ a в предпорядке.

LaTeX

$$$\forall {a,b:\ Specialization(\alpha)},\; ofEquiv(a) \triangleright toEquiv(b) \iff b \le a$$$

Lean4

@[simp]
theorem ofEquiv_specializes_ofEquiv {a b : Specialization α} : ofEquiv a ⤳ ofEquiv b ↔ b ≤ a :=
  Iff.rfl

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

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

Разделы

Аффилиация

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