toSet_sInter — Mathlib

English

The toSet of an intersection (nonempty) equals the intersection of the toSet images.

Русский

toSet пересечения (непустого) равно пересечению изображений toSet.

LaTeX

$$$ \forall x \,( x .Nonempty ) \Rightarrow x.sInter.toSet = (\mathrm{image} (\mathrm{toSet}) x.toSet).sInter $$$

Lean4

theorem toSet_sInter {x : ZFSet.{u}} (h : x.Nonempty) : (⋂₀ x).toSet = ⋂₀ (toSet '' x.toSet) :=
  by
  ext
  simp [mem_sInter h]

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