English
Let x,y be Class with x.Nonempty. Then y ∈ ⋂₀ x if and only if for all z ∈ x, z contains y.
Русский
Пусть x,y — класс и x непуст. Тогда y ∈ ⋂₀ x тогда и только тогда, когда для всех z ∈ x выполняется y ∈ z.
LaTeX
$$$ x\\text{ nonempty } \\Rightarrow y \\in \\bigcap_{0} x \\iff \\forall z, z \\in x \\rightarrow y \\in z. $$$
Lean4
theorem mem_sInter {x y : Class.{u}} (h : x.Nonempty) : y ∈ ⋂₀ x ↔ ∀ z, z ∈ x → y ∈ z :=
by
refine ⟨fun hy z => mem_of_mem_sInter hy, fun H => ?_⟩
simp_rw [mem_def, sInter_apply]
obtain ⟨z, hz⟩ := h
obtain ⟨y, rfl, _⟩ := H z (coe_mem.2 hz)
refine ⟨y, rfl, fun w hxw => ?_⟩
simpa only [coe_mem, coe_apply] using H w (coe_mem.2 hxw)
