mem_sUnion — Mathlib

English

An element y belongs to the sUnion of x iff there exists z ∈ x with 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 : PSet.{u}}, y ∈ ⋃₀ x ↔ ∃ z ∈ x, y ∈ z
  | ⟨α, A⟩, y =>
    ⟨fun ⟨⟨a, c⟩, (e : Equiv y ((A a).Func c))⟩ =>
      have : Func (A a) c ∈ mk (A a).Type (A a).Func := Mem.mk (A a).Func c
      ⟨_, Mem.mk _ _, (Mem.congr_left e).2 (by rwa [eta] at this)⟩,
      fun ⟨⟨β, B⟩, ⟨a, (e : Equiv (mk β B) (A a))⟩, ⟨b, yb⟩⟩ =>
      by
      rw [← eta (A a)] at e
      exact
        let ⟨βt, _⟩ := e
        let ⟨c, bc⟩ := βt b
        ⟨⟨a, c⟩, yb.trans bc⟩⟩

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