English
For any a ∈ EReal with a ≠ ⊤ and any n ∈ ℕ, there exists m ∈ ℕ such that a · n ≤ m.
Русский
Для любого a ∈ EReal с a ≠ ⊤ и любого n ∈ ℕ существует m ∈ ℕ такое, что a · n ≤ m.
LaTeX
$$$ \forall a \in \mathrm{EReal},\ a \neq \top \Rightarrow \forall n \in \mathbb{N}, \exists m \in \mathbb{N},\ a \cdot n \le m $$$
Lean4
theorem exists_nat_ge_mul {a : EReal} (ha : a ≠ ⊤) (n : ℕ) : ∃ m : ℕ, a * n ≤ m :=
match a with
| ⊤ => ha.irrefl.rec
| ⊥ => ⟨0, Nat.cast_zero (R := EReal) ▸ mul_nonpos_iff.2 (.inr ⟨bot_le, n.cast_nonneg'⟩)⟩
| (a : ℝ) => by
obtain ⟨m, an_m⟩ := exists_nat_ge (a * n)
use m
rwa [← coe_coe_eq_natCast n, ← coe_coe_eq_natCast m, ← EReal.coe_mul, EReal.coe_le_coe_iff]
