image_val_sInter — Mathlib

English

For a nonempty family T, the image of the intersection equals the intersection of the images.

Русский

Для непустого семейства T образ пересечения равен пересечению образов.

LaTeX

$$$\\operatorname{image}(\\operatorname{val})(\\bigcap_0 T) = \\bigcap_0 \\{ \\operatorname{image}(\\operatorname{val}) B \\mid B \\in T \\}$, with T.Nonempty$$

Lean4

@[simp]
theorem image_val_sInter (hT : T.Nonempty) : (↑(⋂₀ T) : Set α) = ⋂₀ {(↑B : Set α) | B ∈ T} := by
  rw [← Set.image, sInter_image, sInter_eq_biInter, Subtype.val_injective.injOn.image_biInter_eq hT]

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