Lax Lean Archive

Local formulas are evaluated in any superset of the ball

Lax185574.LocalSubstructure · concepts/Lax185574/LocalSubstructure.lean · lax-185574

proven

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Lemma

    Let φ(x̄) be an r-local σ-formula, let A be a σ-structure, let ā ∈ V(A)^{|x̄|}, and let Ball^A_r(ā) ⊆ B ⊆ V(A). Then A ⊨ φ(ā) if and only if A[B] ⊨ φ(ā).

    Concept map
    3 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    Each proof establishes this claim relative to its assumptions.

    In the paper

    • page 62 of this submission's paper

    Lean source view on GitHub

    1import Lax185574.LocalFormulas
    2
    3/-!
    4---
    5title: Local formulas are evaluated in any superset of the ball
    6type: lemma
    7---
    8Let φ(x̄) be an r-local σ-formula, let A be a σ-structure, let
    9ā ∈ V(A)^{|x̄|}, and let Ball^A_r(ā) ⊆ B ⊆ V(A). Then
    10A ⊨ φ(ā) if and only if A[B] ⊨ φ(ā).
    11
    12# Formalization notes
    13
    14The signature is a finite relational language, as required by the
    15definition of local formulas. The structure is arbitrary, possibly
    16infinite. The tuple is given as a tuple of B, and its image in A is its
    17coordinatewise image. The formula is evaluated in A[B] with the induced
    18structure of `GaifmanGraph.induced`, whose Gaifman graph may have fewer
    19edges than the restriction of the Gaifman graph of A to B.
    20-/
    21
    22namespace Lax185574.LocalSubstructure
    23
    24open FirstOrder FirstOrder.Language
    25open Lax185574.GaifmanGraph Lax185574.LocalFormulas
    26
    27universe u v z
    28
    29/-- **Local formulas and substructures.** An `r`-local formula holds of
    30a tuple in a structure `A` if and only if it holds of the tuple in every
    31induced substructure `A[B]` with `B ⊇ Ball^A_r(ā)`. -/
    32axiom realize_iff_realize_induced (L : Language.{u, v}) [L.IsRelational]
    33 [Finite (Σ l, L.Relations l)] (r k : ℕ) (φ : L.Formula (Fin k)) (hφ : IsLocal r φ)
    34 (V : Type z) [L.Structure V] (B : Set V) (a : Fin k → B) :
    35 ball L r (Subtype.val ∘ a) ⊆ B →
    36 (φ.Realize (Subtype.val ∘ a) ↔ @Formula.Realize L B (induced B) _ φ a)
    37
    38end Lax185574.LocalSubstructure
    39
    Show Proof
    Formalization notes

    The signature is a finite relational language, as required by the definition of local formulas. The structure is arbitrary, possibly infinite. The tuple is given as a tuple of B, and its image in A is its coordinatewise image. The formula is evaluated in A[B] with the induced structure of GaifmanGraph.inducedGaifmanGraph.induced, whose Gaifman graph may have fewer edges than the restriction of the Gaifman graph of A to B.

    Builds on
    Used by

    none

    From Mathlib

    none

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…