mem_support_bindOnSupport_iff — Mathlib

English

An outcome b belongs to the support of p.bindOnSupport f if and only if there exists some a ∈ supp(p) such that b belongs to the support of f(a, ha).

Русский

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

LaTeX

$$$$ b \\in \\mathrm{supp}(p.bindOnSupport f) \\;\\Leftrightarrow\\; \\exists a \\in \\mathrm{supp}(p), \\; b \\in \\mathrm{supp}(f(a, ha)). $$$$

Lean4

theorem mem_support_bindOnSupport_iff (b : β) :
    b ∈ (p.bindOnSupport f).support ↔ ∃ (a : α) (h : a ∈ p.support), b ∈ (f a h).support := by
  simp only [support_bindOnSupport, Set.mem_iUnion]

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