image_subtype_univ_ssubset_image_univ

English

If k ∈ image b univ and not p(k), then the image of the restricted domain { a | p(b(a)) } under b is a proper subset of image b univ.

Русский

Пусть k лежит в образе b(умноженная единица) и не выполняется p(k). Тогда изображение функции b на подтипе { a | p(b(a)) } является строгим подмножеством изображения b на all-univ.

LaTeX

$$$$ \\operatorname{image}( \\lambda i : \\{ a \\mid p(b a) \\}, b i) \\, \\operatorname{univ} \\subsetneq \\operatorname{image} b \\operatorname{univ}. $$$$

Lean4

theorem image_subtype_univ_ssubset_image_univ [Fintype α] [DecidableEq β] (k : β) (b : α → β)
    (hk : k ∈ Finset.image b univ) (p : β → Prop) [DecidablePred p] (hp : ¬p k) :
    image (fun i : { a // p (b a) } => b ↑i) univ ⊂ image b univ := by grind

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