eval_image_piFinset_const — Mathlib

English

Same as above, with a strengthened existence condition; the image equals t(a).

Русский

То же самое с усиленным условием существования; образ равен t(a).

LaTeX

$$$\\forall a,\\ [\\forall b\\ (b \\neq a \\Rightarrow (t(b)).Nonempty)] \\Rightarrow \\operatorname{image}(\\lambda f. f(a))(\\operatorname{piFinset} t) = t(a).$$$

Lean4

theorem eval_image_piFinset_const {β} [DecidableEq β] (t : Finset β) (a : α) :
    ((piFinset fun _i : α ↦ t).image fun f ↦ f a) = t :=
  by
  obtain rfl | ht := t.eq_empty_or_nonempty
  · haveI : Nonempty α := ⟨a⟩
    simp
  · exact eval_image_piFinset (fun _ ↦ t) a fun _ _ ↦ ht

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