English
For all m,n, n = 1 or m ≤ minFac(n) iff for all primes p dividing n, m ≤ p.
Русский
Для всех m,n: n = 1 или m ≤ minFac(n) тогда и только тогда, когда для каждого простого p, делящего n, выполняется m ≤ p.
LaTeX
$$$\\\\forall m,n \\\\in \\\\mathbb{N}, \\\\; (n = 1 \\\\lor \\\\; m \\\\le \\\\minFac(n)) \\\\iff \\\\forall p \\\\in \\\\mathbb{N}, \\\\mathrm{Prime}(p) \\\\rightarrow (p \\\\mid n \\\\Rightarrow m \\\\le p).$$$
Lean4
theorem le_minFac {m n : ℕ} : n = 1 ∨ m ≤ minFac n ↔ ∀ p, Prime p → p ∣ n → m ≤ p :=
⟨fun h p pp d => h.elim (by rintro rfl; cases pp.not_dvd_one d) fun h => le_trans h <| minFac_le_of_dvd pp.two_le d,
fun H => or_iff_not_imp_left.2 fun n1 => H _ (minFac_prime n1) (minFac_dvd _)⟩
