instIsSuccArchimedeanOrderDual

Mathlib.Order.SuccPred.Archimedean

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

English

In the dual order (order on αᵒᵈ), if v1 ≤ r and v2 ≤ r, then v1 ≤ v2 or v2 ≤ v1.

Русский

В двойном порядке (αᵒᵈ), если v1 ≤ r и v2 ≤ r, то либо v1 ≤ v2, либо v2 ≤ v1.

LaTeX

$$$\forall r,v_1,v_2:\alpha,\ (v_1 \le r) \land (v_2 \le r) \Rightarrow (v_1 \le v_2) \lor (v_2 \le v_1)$$$

Lean4

instance : IsSuccArchimedean αᵒᵈ :=
  ⟨fun {a b} h => by convert exists_pred_iterate_of_le h.ofDual⟩

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

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

Разделы

Аффилиация

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