not_pseudoperfect_iff_forall — Mathlib

English

Not pseudoperfect n is equivalent to either n = 0 or every subset of proper divisors has sum ≠ n.

Русский

Не псевдоперфектно n эквивалентно либо n = 0, либо для каждого подмножества делителей n сумма не равна n.

LaTeX

$$¬Pseudoperfect(n) ↔ n = 0 ∨ ∀ s ⊆ properDivisors(n), ∑ i ∈ s i ≠ n$$

Lean4

theorem not_pseudoperfect_iff_forall : ¬Pseudoperfect n ↔ n = 0 ∨ ∀ s ⊆ properDivisors n, ∑ i ∈ s, i ≠ n :=
  by
  rw [Pseudoperfect, not_and_or]
  simp only [not_lt, nonpos_iff_eq_zero, not_exists, not_and, ne_eq]

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