mem_sUnion — Mathlib

English

For y ∈ ⋃₀ x, there exists z ∈ x such that y ∈ z.

Русский

Если y принадлежит объединению ⋃₀ x, то существует z ∈ x такое, что y ∈ z.

LaTeX

$$$ y \in \bigcup\!_0 x \iff \exists z \in x, y \in z $$$

Lean4

@[simp]
theorem mem_sUnion {x y : ZFSet.{u}} : y ∈ ⋃₀ x ↔ ∃ z ∈ x, y ∈ z :=
  Quotient.inductionOn₂ x y fun _ _ =>
    PSet.mem_sUnion.trans ⟨fun ⟨z, h⟩ => ⟨⟦z⟧, h⟩, fun ⟨z, h⟩ => Quotient.inductionOn z (fun z h => ⟨z, h⟩) h⟩

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