eq_of_le_of_forall_lt_imp_le_of_dense

English

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

Русский

Если a₂ ≤ a₁ и для всех a < a₁ выполняется a ≤ a₂, то a₁ = a₂.

LaTeX

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

Lean4

theorem eq_of_le_of_forall_lt_imp_le_of_dense (h₁ : a₂ ≤ a₁) (h₂ : ∀ a, a₂ < a → a₁ ≤ a) : a₁ = a₂ :=
  le_antisymm (le_of_forall_gt_imp_ge_of_dense h₂) h₁

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