le_of_forall_lt_iff_le — Mathlib

English

In a linear densely ordered type with no minimum, (∀ z, x < z → y ≤ z) if and only if y ≤ x.

Русский

В линейном плотно упорядоченном множестве без минимума: (∀ z, x < z → y ≤ z) эквивалентно y ≤ x.

LaTeX

$$$(\forall z : α, x < z \rightarrow y ≤ z) \iff y ≤ x$$$

Lean4

theorem le_of_forall_lt_iff_le : (∀ z : α, x < z → y ≤ z) ↔ y ≤ x := by
  cases x <;> cases y <;> simp [exists_lt, forall_gt_imp_ge_iff_le_of_dense]

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