coe_sInter — Mathlib

English

If x is a nonempty collection of ZFSets, then ↑(⋂₀ x) = ⋂₀ (x : Class).

Русский

Если x — непустое множество ZFSet, то ↑(⋂₀ x) = ⋂₀ (x : Class).

LaTeX

$$$ x \\text{ Nonempty } \\Rightarrow \\uparrow(\\bigcap_{0} x) = \\bigcap_{0} (x : \\mathrm{Class}). $$$

Lean4

@[simp, norm_cast]
theorem coe_sInter {x : ZFSet.{u}} (h : x.Nonempty) : ↑(⋂₀ x : ZFSet) = ⋂₀ (x : Class.{u}) :=
  Set.ext fun _ => (ZFSet.mem_sInter h).trans sInter_apply.symm

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