divisors_subset_properDivisors — Mathlib

English

If n ≠ 0, m | n, and m ≠ n, then divisors(m) ⊆ properDivisors(n).

Русский

Если n ≠ 0, m | n и m ≠ n, то делители m входят в properDivisors(n).

LaTeX

$$$n\\neq 0 \\land m|n \\land m\\neq n \\Rightarrow \\text{divisors}(m) \\subseteq \\text{properDivisors}(n)$$$

Lean4

theorem divisors_subset_properDivisors {m : ℕ} (hzero : n ≠ 0) (h : m ∣ n) (hdiff : m ≠ n) :
    divisors m ⊆ properDivisors n := by
  apply Finset.subset_iff.2
  intro x hx
  exact
    Nat.mem_properDivisors.2
      ⟨(Nat.mem_divisors.1 hx).1.trans h,
        lt_of_le_of_lt (divisor_le hx) (lt_of_le_of_ne (divisor_le (Nat.mem_divisors.2 ⟨h, hzero⟩)) hdiff)⟩

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