instHasIsosMin — Mathlib

English

If J and K are precoverages with isomorphisms available, then their meet J ⊓ K also has isomorphisms, with the property that an arrow is an isomorphism in J ⊓ K exactly when it is an isomorphism in both J and K.

Русский

Если J и K — предпокрытия с разрешёнными изоморфизмами, то их барицентр J ⊓ K тоже имеет изоморфизмы; стрелка является изоморфизмом в J ⊓ K тогда и только тогда, когда она является изоморфизмом и в J, и в K.

LaTeX

$$$ (J \\sqcap K) \\text{ HasIsos} \\quad\\text{iff} \\quad J \\text{ HasIsos} \\land K \\text{ HasIsos}$$$

Lean4

instance (J K : Precoverage C) [HasIsos J] [HasIsos K] : HasIsos (J ⊓ K) where
  mem_coverings_of_isIso f _ := ⟨mem_coverings_of_isIso f, mem_coverings_of_isIso f⟩

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