mem_pmap — Mathlib

English

An element b belongs to pmap f s H if and only if there exists an a ∈ s and a witness h that yields b = f(a, H a h).

Русский

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

LaTeX

$$$b\\in\\operatorname{pmap}f s H \\iff \\exists a\\in s, f(a, H(a,h))=b$$$

Lean4

@[simp]
theorem mem_pmap {p : α → Prop} {f : ∀ a, p a → β} {s H b} : b ∈ pmap f s H ↔ ∃ (a : _) (h : a ∈ s), f a (H a h) = b :=
  Quot.inductionOn s (fun _l _H => List.mem_pmap) H

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