mem_pmap_iff — Mathlib

English

Let f : ∀ a, P a → β and z ∈ Sym2 α with h : ∀ a ∈ z, P a. Then b ∈ z.pmap f h iff ∃ a ∈ z, b = f a (h a ha).

Русский

Пусть f: ∀ a, P a → β и z ∈ Sym2 α с h: ∀ a ∈ z, P a. Тогда b ∈ z.pmap f h эквивалентно ∃ a ∈ z: b = f a (h a ha).

LaTeX

$$$ b \\in z.pmap f h \\iff \\exists a \\in z, b = f a (h a ha). $$$

Lean4

@[simp]
theorem mem_pmap_iff {P : α → Prop} (f : ∀ a, P a → β) (z : Sym2 α) (h : ∀ a ∈ z, P a) (b : β) :
    b ∈ z.pmap f h ↔ ∃ (a : α) (ha : a ∈ z), b = f a (h a ha) :=
  by
  obtain ⟨x, y⟩ := z
  rw [pmap_pair f x y h]
  aesop

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