mem_bind — Mathlib

English

A point b lies in the bind q f iff there exists a ∈ q with b ∈ f a.

Русский

Точка b принадлежит объединению bind q f тогда и только тогда, когда существует a ∈ q такое, что b ∈ f(a).

LaTeX

$$$b \in bind\ q\ f \iff \exists a \in q, \, b \in f\, a$$$

Lean4

@[simp]
theorem mem_bind (q : Semiquot α) (f : α → Semiquot β) (b : β) : b ∈ bind q f ↔ ∃ a ∈ q, b ∈ f a := by
  simp_rw [← exists_prop]; exact Set.mem_iUnion₂

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