mem_bind — Mathlib

English

Membership in (P.bind Q).parts is equivalent to the existence of A with b ∈ (Q A hA).parts.

Русский

Членство в (P.bind Q).parts эквивалентно существованию A, для которого b ∈ (Q A hA).parts.

LaTeX

$$$b \in (P.bind Q).parts \iff \exists A, hA, b \in (Q A hA).parts$$$

Lean4

theorem mem_bind : b ∈ (P.bind Q).parts ↔ ∃ A hA, b ∈ (Q A hA).parts :=
  by
  rw [bind, mem_biUnion]
  constructor
  · rintro ⟨⟨A, hA⟩, -, h⟩
    exact ⟨A, hA, h⟩
  · rintro ⟨A, hA, h⟩
    exact ⟨⟨A, hA⟩, mem_attach _ ⟨A, hA⟩, h⟩

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