isAmalgamation_sieveExtend — Mathlib

English

If x is an amalgamation for t with respect to R, then the extended family x.sieveExtend is also an amalgamation for t; i.e., x.sieveExtend.IsAmalgamation t.

Русский

Если x амальгамма для t по R, то x.sieveExtend также амальгамма для t.

LaTeX

$$x.IsAmalgamation t → x.sieveExtend.IsAmalgamation t$$

Lean4

theorem isAmalgamation_sieveExtend {R : Presieve X} (x : FamilyOfElements P R) (t : P.obj (op X))
    (ht : x.IsAmalgamation t) : x.sieveExtend.IsAmalgamation t :=
  by
  intro Y f hf
  dsimp [FamilyOfElements.sieveExtend]
  rw [← ht _, ← FunctorToTypes.map_comp_apply, ← op_comp, hf.choose_spec.choose_spec.choose_spec.2]

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