instIsStableUnderBaseChangeMin — Mathlib

English

The intersection J ⊓ K of two base-change stable precoverages is itself stable under base change.

Русский

Пересечение J ⊓ K двух основанных на изменении базы покрытий сохраняет стабильность под базовым изменением.

LaTeX

$$$ (J \\sqcap K) \\text{ IsStableUnderBaseChange}$$$

Lean4

instance (J K : Precoverage C) [IsStableUnderBaseChange.{w} J] [IsStableUnderBaseChange.{w} K] :
    IsStableUnderBaseChange.{w} (J ⊓ K) where
  mem_coverings_of_isPullback _ hf _ _ _ _ _
    h := ⟨mem_coverings_of_isPullback _ hf.1 _ _ _ h, mem_coverings_of_isPullback _ hf.2 _ _ _ h⟩

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