mem_sInter — Mathlib

English

If x is nonempty, then y ∈ ⋂₀ x iff ∀ z ∈ x, y ∈ z.

Русский

Если x непусто, то y ∈ ⋂₀ x тогда и только тогда, когда для всякого z ∈ x имеет место y ∈ z.

LaTeX

$$$ x.Nonempty \Rightarrow y \in \bigcap_0 x \iff \forall z \in x, y \in z $$$

Lean4

theorem mem_sInter {x y : ZFSet} (h : x.Nonempty) : y ∈ ⋂₀ x ↔ ∀ z ∈ x, y ∈ z :=
  by
  unfold sInter
  simp only [and_iff_right_iff_imp, mem_sep]
  intro mem
  apply mem_sUnion.mpr
  replace ⟨s, h⟩ := h
  exact ⟨_, h, mem _ h⟩

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