mem_biUnion — Mathlib

English

An element b belongs to s.biUnion t iff there exists a in s with b ∈ t(a).

Русский

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

LaTeX

$$$b \\in s.biUnion t \\iff \\exists a \\in s, b \\in t a$$$

Lean4

@[simp, grind =]
theorem mem_biUnion {b : β} : b ∈ s.biUnion t ↔ ∃ a ∈ s, b ∈ t a := by
  simp only [mem_def, biUnion_val, Multiset.mem_dedup, Multiset.mem_bind]

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