Lax Lean Archive

Invariance and characterization of containment

Lax420092.ContainmentInvariance · concepts/Lax420092/ContainmentInvariance.lean · lax-420092

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

    Containment of the left query in the right one is invariant under isomorphism of pairs, and a pair is a yes-instance of CQContainment exactly when its left query is contained in its right query.

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

    This concept declares 2 statements. Each proof establishes one of them relative to its assumptions.

    1 cqContainment_iff proven

    2 queryContained_iso proven

    Lean source view on GitHub

    1import Lax904597.Problems
    2import Lax904597.Interpretations
    3import Lax904597.Classes
    4import Lax799700.Problems
    5import Lax420092.QueryDatabases
    6import Lax420092.Evaluation
    7import Lax420092.QueryPairs
    8import Lax420092.PackagedInstances
    9
    10/-!
    11---
    12title: Invariance and characterization of containment
    13type: lemma
    14---
    15Containment of the left query in the right one is invariant under isomorphism
    16of pairs, and a pair is a yes-instance of CQContainment exactly when its left
    17query is contained in its right query.
    18-/
    19
    20namespace Lax420092.ContainmentInvariance
    21
    22open FirstOrder FirstOrder.Language
    23open Lax904597.Problems Lax904597.Interpretations Lax904597.Classes Lax799700.Problems
    24open Lax420092.QueryDatabases Lax420092.Evaluation Lax420092.QueryPairs Lax420092.PackagedInstances
    25
    26/-- The property `QueryContained` is isomorphism-invariant. -/
    27axiom queryContained_iso : ∀ {A B : Type} [queryPair.Structure A] [queryPair.Structure B],
    28 (A ≃[queryPair] B) → (QueryContained A ↔ QueryContained B)
    29
    30/-- The yes-instances of CQContainment are exactly the pairs whose left query
    31is contained in the right one. -/
    32axiom cqContainment_iff : ∀ (A : Type) [queryPair.Structure A],
    33 CQContainment A ↔ QueryContained A
    34
    35end Lax420092.ContainmentInvariance
    36
    Show ProofShow Proof
    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…