image_biInter_eq — Mathlib

English

If there exists i with property p i and f is injOn on a union of s i hi, then the image of the bi-Inter equals the bi-Inter of the images.

Русский

Если существует i с свойством p i и f инъективно на объединении s i hi, тогда образ biInter равен biInter образов.

LaTeX

$$$\\text{image_biInter_eq}$$$

Lean4

theorem image_biInter_eq {p : ι → Prop} {s : ∀ i, p i → Set α} (hp : ∃ i, p i) {f : α → β}
    (h : InjOn f (⋃ (i) (hi), s i hi)) : (f '' ⋂ (i) (hi), s i hi) = ⋂ (i) (hi), f '' s i hi :=
  by
  simp only [iInter, iInf_subtype']
  haveI : Nonempty { i // p i } := nonempty_subtype.2 hp
  apply InjOn.image_iInter_eq
  simpa only [iUnion, iSup_subtype'] using h

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