subset_univ_image_iff — Mathlib

English

A special case of the above for sets: a finite set t is contained in the image of a set under f iff t is the image of a finite subset of that set.

Русский

Особый случай выше для множеств: множество t ⊆ f[s] тогда и только тогда, когда t = f[s'] для некоторого конечного подмножества s' ⊆ s.

LaTeX

$$$t \\subseteq f(\\,s\\,) \\iff \\exists s'\\subseteq s,\\, f(s') = t$$$

Lean4

/-- A special case of `subset_image_iff`,
which corresponds to `Set.subset_range_iff_exists_image_eq` for `Set`.
-/
theorem subset_univ_image_iff [Fintype α] [DecidableEq β] {t : Finset β} {f : α → β} :
    t ⊆ univ.image f ↔ ∃ s' : Finset α, s'.image f = t := by simp [subset_image_iff]

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