mem_bind — Mathlib

English

A more explicit version of mem_bind: s ∈ bind f m iff ∃ t ∈ f with ∀ x ∈ t, s ∈ m x.

Русский

Более явная версия mem_bind: s ∈ bind f m эквивалентно ∃ t ∈ f, ∀ x ∈ t, s ∈ m x.

LaTeX

$$$s \\in \\mathrm{bind} f m \\iff \\exists t \\in f, \\forall x \\in t, s \\in m x$$$

Lean4

@[simp]
theorem mem_bind {s : Set β} {f : Filter α} {m : α → Filter β} : s ∈ bind f m ↔ ∃ t ∈ f, ∀ x ∈ t, s ∈ m x :=
  calc
    s ∈ bind f m ↔ {a | s ∈ m a} ∈ f := Iff.rfl
    _ ↔ ∃ t ∈ f, t ⊆ {a | s ∈ m a} := exists_mem_subset_iff.symm
    _ ↔ ∃ t ∈ f, ∀ x ∈ t, s ∈ m x := Iff.rfl

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