eval_image_piFinset_subset — Mathlib

English

For a, the set of all f(a) with f ∈ piFinset t is contained in t(a).

Русский

Образ координаты a из piFinset t подмножество t(a).

LaTeX

$$$\\bigl(\\operatorname{piFinset} t\\bigr).{\\text{image}}(\\lambda f\\mapsto f(a)) \\subseteq t(a).$$$

Lean4

theorem eval_image_piFinset_subset (t : ∀ a, Finset (δ a)) (a : α) [DecidableEq (δ a)] :
    ((piFinset t).image fun f ↦ f a) ⊆ t a :=
  image_subset_iff.2 fun _x hx ↦ mem_piFinset.1 hx _

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