eq_of_forall_natCast_le_iff — Mathlib

English

If for all a ∈ ℕ, a ≤ m ↔ a ≤ n, then m = n.

Русский

Если для всех a ∈ ℕ выполняется a ≤ m ↔ a ≤ n, то m = n.

LaTeX

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

Lean4

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

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