eq_of_le_of_forall_gt_imp_ge_of_dense

English

If a₂ ≤ a₁ and ∀ a, a₂ < a → a ≤ a₁, then a₁ = a₂.

Русский

Если a₂ ≤ a₁ и для каждого a, если a₂ < a, то a ≤ a₁, тогда a₁ = a₂.

LaTeX

$$$a_2 \le a_1 \text{ and } (\forall a)(a_2 < a \rightarrow a \le a_1) \Rightarrow a_1 = a_2$$$

Lean4

theorem eq_of_le_of_forall_gt_imp_ge_of_dense (h₁ : a₂ ≤ a₁) (h₂ : ∀ a < a₁, a ≤ a₂) : a₁ = a₂ :=
  (le_of_forall_lt_imp_le_of_dense h₂).antisymm h₁

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