equitableOn_iff_exists_image_subset_icc

English

EquitableOn(s,f) is equivalent to the image of s under f being contained in a closed interval Icc(b,b+1) for some b.

Русский

EquitableOn(s,f) эквивалентно тому, что изображение s под действием f содержится в замкнутом интервале Icc(b,b+1) для некоторого b.

LaTeX

$$$s.\mathrm{EquitableOn} f \iff \exists b, f''s \subseteq \mathrm{Icc}(b, b+1)$$$

Lean4

theorem equitableOn_iff_exists_image_subset_icc {s : Set α} {f : α → ℕ} :
    s.EquitableOn f ↔ ∃ b, f '' s ⊆ Icc b (b + 1) := by
  simpa only [image_subset_iff] using equitableOn_iff_exists_le_le_add_one

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