isSupported_int — Mathlib

English

For every integer i, the embedded element i is supported on any s.

Русский

Для каждого целого i встроенный элемент i поддержан на любом s.

LaTeX

$$$ \\text{IsSupported}(i, s) \\text{ for } i \\in \\mathbb{Z} $$$

Lean4

theorem isSupported_int {i : ℤ} {s : Set α} : IsSupported (↑i) s :=
  Int.induction_on i isSupported_zero
    (fun i hi => by rw [Int.cast_add, Int.cast_one]; exact isSupported_add hi isSupported_one) fun i hi => by
    rw [Int.cast_sub, Int.cast_one]; exact isSupported_sub hi isSupported_one

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