ge_of_forall_gt_iff_ge — Mathlib

English

Let x and y be elements of the extended order WithTop α. Then x ≤ y if and only if for every a in α, a < x implies a ≤ y.

Русский

Пусть x и y принадлежат расширенному порядку WithTop α. Тогда x ≤ y тогда и только тогда, когда для каждого a ∈ α выполняется a < x ⇒ a ≤ y.

LaTeX

$$$x \\le y \\iff \\forall a:\\\\alpha,\\; a < x \\rightarrow a \\le y$$$

Lean4

theorem ge_of_forall_gt_iff_ge : (∀ a : α, a < x → a ≤ y) ↔ x ≤ y := by
  cases x <;> cases y <;> simp [exists_gt, forall_lt_imp_le_iff_le_of_dense]

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