range_coind — Mathlib

English

Let f: α → β and h a predicate on β with h(a) for all a. Then range(Subtype.coind f h) equals the preimage of range f under Subtype.val.

Русский

Пусть f: α → β и h: β → Prop удовлетворяющий h(f(a)) для всех a. Тогда range(Subtype.coind f h) совпадает с preimage range f по Subtype.val.

LaTeX

$$$$\\mathrm{range}(\\mathrm{Subtype.coind}(f,h)) = (\\mathrm{Subtype.val})^{-1}(\\mathrm{range}(f)).$$$$

Lean4

theorem range_coind (f : α → β) {p : β → Prop} (h : ∀ (a : α), p (f a)) :
    range (Subtype.coind f h) = Subtype.val ⁻¹' range f := by simp [Set.ext_iff, Subtype.ext_iff]

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