exists — Mathlib

English

For any predicate p on the total space, there exists a point x with p(x) if and only if there exist a base point b and a fiber element y with p(⟨b,y⟩).

Русский

Для любого предиката p на просторe всего пространства существует точка x с p(x) тогда и только тогда, когда существуют базовая точка b и элемент волокна y such that p(⟨b,y⟩).

LaTeX

$$$$\exists x:\, \text{TotalSpace } F E,\ p(x)\;\iff\;\exists b:\, B,\exists y:\, E(b),\ p(\langle b,y\rangle).$$$$

Lean4

@[simp]
theorem «exists» {p : TotalSpace F E → Prop} : (∃ x, p x) ↔ ∃ b y, p ⟨b, y⟩ :=
  ⟨fun ⟨x, hx⟩ ↦ ⟨x.1, x.2, hx⟩, fun ⟨b, y, h⟩ ↦ ⟨⟨b, y⟩, h⟩⟩

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