exists — Mathlib

English

For a bijection f on s to t, the existence of b in t with property P corresponds to the existence of a in s with P(f(a)).

Русский

Для биекции f на s→t существование b∈t с свойством P эквивалентно существованию a∈s с P(f(a)).

LaTeX

$$$\\text{BijOn}(f,s,t) \\Longrightarrow (\\exists b\\in t, P(b)) \\iff (\\exists a\\in s, P(f(a)))$$$

Lean4

theorem «exists» {p : β → Prop} (hf : BijOn f s t) : (∃ b ∈ t, p b) ↔ ∃ a ∈ s, p (f a)
    where
  mp := by rintro ⟨b, hb, h⟩; obtain ⟨a, ha, rfl⟩ := hf.surjOn hb; exact ⟨a, ha, h⟩
  mpr := by rintro ⟨a, ha, h⟩; exact ⟨f a, hf.mapsTo ha, h⟩

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