forall — Mathlib

English

For any property p on opens, (for all U, p U) is equivalent to (for all open sets U represented as sets, p ⟨U, IsOpen U⟩).

Русский

Для любого свойства p над открытыми, выполняется эквивалентность: для всех U, p U же для всех U, представленного как пара (U, IsOpen U).

LaTeX

$$$\bigl( \forall U:\mathrm{Opens}(\alpha), p(U) \bigr) \;\Leftrightarrow\; \bigl( \forall U:\mathrm{Set}(\alpha), \forall hU: IsOpen(U), p(\langle U,hU\rangle) \bigr).$$$

Lean4

theorem «forall» {p : Opens α → Prop} : (∀ U, p U) ↔ ∀ (U : Set α) (hU : IsOpen U), p ⟨U, hU⟩ :=
  ⟨fun h _ _ => h _, fun h _ => h _ _⟩

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