image_finset_of_le — Mathlib

English

If a finite Finset s is pairwise disjoint under f and g(a) ≤ f(a), then the image under g of s is pairwise disjoint under f.

Русский

Если конечное множество s пары с f и g удовлетворяют g(a) ≤ f(a), то образ s под g образует попарно непересекающееся множество относительно f.

LaTeX

$$(s.toSet).PairwiseDisjoint f → (∀ a, f(g a) ≤ f a) → (s.image g).toSet.PairwiseDisjoint f$$

Lean4

theorem image_finset_of_le [DecidableEq ι] {s : Finset ι} {f : ι → α} (hs : (s : Set ι).PairwiseDisjoint f) {g : ι → ι}
    (hf : ∀ a, f (g a) ≤ f a) : (s.image g : Set ι).PairwiseDisjoint f :=
  by
  rw [coe_image]
  exact hs.image_of_le hf

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