le_antisymm

Mathlib.Algebra.Order.CauSeq.Basic

URI: https://scilib.ai/kg/mathlib#CauSeq.le_antisymm

English

If f ≤ g and g ≤ f, then f ≈ g.

Русский

Если f ≤ g и g ≤ f, то f ≈ g.

LaTeX

$$$\bigl(f \le g\bigr) \land \bigl(g \le f\bigr) \Rightarrow f \approx g.$$$

Lean4

theorem le_antisymm {f g : CauSeq α abs} (fg : f ≤ g) (gf : g ≤ f) : f ≈ g :=
  fg.resolve_left (not_lt_of_ge gf)

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

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

Разделы

Аффилиация

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