mem_biUnion — Mathlib

English

Let s : Set α, t : α → Set β, x : α, y : β. If x ∈ s and y ∈ t x, then y ∈ ⋃ x ∈ s, t x.

Русский

Пусть s ⊆ α, t : α → Set β, x ∈ s и y ∈ t x; тогда y принадлежит ⋃_{x ∈ s} t x.

LaTeX

$$$$\\text{If } x \\in s \\text{ and } y \\in t(x), \\text{ then } y \\in \\bigcup_{x \\in s} t(x).$$$$

Lean4

/-- A specialization of `mem_iUnion₂`. -/
theorem mem_biUnion {s : Set α} {t : α → Set β} {x : α} {y : β} (xs : x ∈ s) (ytx : y ∈ t x) : y ∈ ⋃ x ∈ s, t x :=
  mem_iUnion₂_of_mem xs ytx

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