isAmalgamation_restrict — Mathlib

English

For presieves R1 ≤ R2 (in a suitable lattice structure), the restricted amalgamation property holds: if x is amalgamating t over R2, then its restriction to R1 is also an amalgamation for t.

Русский

Для R1 ≤ R2 в подходящей решётке верно, что если x амальгаммает t над R2, то её ограничение к R1 тоже амальгамма для t.

LaTeX

$$∑(h:R1≤R2) (x.IsAmalgamation t) → ((x.restrict h).IsAmalgamation t)$$

Lean4

theorem isAmalgamation_restrict {R₁ R₂ : Presieve X} (h : R₁ ≤ R₂) (x : FamilyOfElements P R₂) (t : P.obj (op X))
    (ht : x.IsAmalgamation t) : (x.restrict h).IsAmalgamation t := fun Y f hf => ht f (h Y hf)

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