forall_natCast_le_iff_le — Mathlib

English

The condition (∀ a : ℕ, a ≤ m → a ≤ n) is equivalent to m ≤ n.

Русский

Условие (∀ a ∈ ℕ, a ≤ m → a ≤ n) эквивалентно m ≤ n.

LaTeX

$$$(\forall a : \mathbb{N}, a \le m \to a \le n) \leftrightarrow m \le n$$$

Lean4

/-- Version of `WithTop.forall_coe_le_iff_le` using `Nat.cast` rather than `WithTop.some`. -/
theorem forall_natCast_le_iff_le : (∀ a : ℕ, a ≤ m → a ≤ n) ↔ m ≤ n :=
  WithTop.forall_coe_le_iff_le

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