inf — Mathlib

English

Let P and Q be morphism properties that are local at the source with respect to a precoverage K. Then their intersection P ⊓ Q is also local at the source with respect to K.

Русский

Пусть P и Q — свойства морфизмов, локальные по источнику относительно предохвата K. Тогда их пересечение P ⊓ Q также локально по источнику относительно K.

LaTeX

$$$ IsLocalAtSource(P \\sqcap Q)\\, K \\quad \\text{provided } IsLocalAtSource(P)\\, K \\text{ and } IsLocalAtSource(Q)\\, K. $$$

Lean4

instance inf (P Q : MorphismProperty C) [IsLocalAtSource P K] [IsLocalAtSource Q K] : IsLocalAtSource (P ⊓ Q) K
    where
  comp 𝒰 i hf := ⟨comp 𝒰 i hf.1, comp 𝒰 i hf.2⟩
  of_zeroHypercover _ h := ⟨of_zeroHypercover _ fun i ↦ (h i).1, of_zeroHypercover _ fun i ↦ (h i).2⟩

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