mem_biInter — Mathlib

English

Let s : Set α, t : α → Set β, y : β. If h : ∀ x ∈ s, y ∈ t x, then y ∈ ⋂ x ∈ s, t x.

Русский

Пусть s ⊆ α, t : α → Set β, y ∈ β. Если для каждого x ∈ s выполняется y ∈ t x, то y принадлежит ⋂ x ∈ s, t x.

LaTeX

$$$$\\left(\\forall x\\in s\\, , y \\in t(x)\\right) \\Rightarrow y \\in \\bigcap_{x \\in s} t(x).$$$$

Lean4

/-- A specialization of `mem_iInter₂`. -/
theorem mem_biInter {s : Set α} {t : α → Set β} {y : β} (h : ∀ x ∈ s, y ∈ t x) : y ∈ ⋂ x ∈ s, t x :=
  mem_iInter₂_of_mem h

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