ofNat_mem — Mathlib

English

For an AddSubmonoidWithOneClass S R, any element of S generated by natural numbers via the OfNat construction lies in S, provided the natural number is at least two.

Русский

Для AddSubmonoidWithOneClass S R любой элемент S, полученный из натурального числа через OfNat, принадлежит S, если число не меньше двух.

LaTeX

$$$ofNat(n) \in S$ for n \ge 2$$

Lean4

@[simp, aesop safe (rule_sets := [SetLike])]
theorem ofNat_mem [AddSubmonoidWithOneClass S R] (s : S) (n : ℕ) [n.AtLeastTwo] : ofNat(n) ∈ s := by
  rw [← Nat.cast_ofNat]; exact natCast_mem s n

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