realize_formula_cast — Mathlib

English

For a formula φ, its realization in the ultraproduct with a family x_i is equivalent to almost-everywhere realization in the components; this is a concise restatement of Łoś's theorem for formulas.

Русский

Для формулы φ реализация в ультропроизведении с семейства x_i эквивалентна почти везде реализации в компонентах; это краткое выражение теоремы Лёша о каждом формуле.

LaTeX

$$$\varphi\text{ Realize }((x_i)) \iff \forall^u a, \varphi\text{ Realize }(x_i(a))$$$

Lean4

theorem realize_formula_cast {β : Type*} (φ : L.Formula β) (x : β → ∀ a, M a) :
    (φ.Realize fun i => (x i : (u : Filter α).Product M)) ↔ ∀ᶠ a : α in u, φ.Realize fun i => x i a :=
  by
  simp_rw [Formula.Realize, ← boundedFormula_realize_cast φ x, iff_eq_eq]
  exact congr rfl (Subsingleton.elim _ _)

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