mem_disjiUnion — Mathlib

English

An element b belongs to disjiUnion s f if and only if there exists a ∈ s with b ∈ f(a).

Русский

Элемент b принадлежит disjiUnion s f тогда и только тогда, когда существует a ∈ s, такое что b ∈ f(a).

LaTeX

$$$ b \\in s.disjiUnion t h \\iff \\exists a \\in s, b \\in t a $$$

Lean4

@[simp, grind =]
theorem mem_disjiUnion {b : β} {h} : b ∈ s.disjiUnion t h ↔ ∃ a ∈ s, b ∈ t a := by
  simp only [mem_def, disjiUnion_val, Multiset.mem_bind]

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