ofLawson_inj

Mathlib.Topology.Order.LawsonTopology

URI: https://scilib.ai/kg/mathlib#Topology.WithLawson.ofLawson_inj

English

The embedding of α into WithLawson α is injective: if ofLawson a = ofLawson b then a = b (for a,b in WithLawson α).

Русский

Встраивание α в WithLawson α инъективно: если ofLawson a = ofLawson b, то a = b (для a,b ∈ WithLawson α).

LaTeX

$$$ofLawson a = ofLawson b \iff a = b$$$

Lean4

theorem ofLawson_inj {a b : WithLawson α} : ofLawson a = ofLawson b ↔ a = b :=
  Iff.rfl

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

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

Разделы

Аффилиация

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