instIsStableUnderSupMin — Mathlib

English

If J and K are stable under suprema, then their infimum J ⊓ K is stable under suprema as well, i.e., sup_mem_coverings is maintained componentwise.

Русский

Если J и K стабильны под супремумами, то их пересечение J ⊓ K тоже стабильно относительно супремумов; свойство sup_mem_coverings сохраняется по компонентам.

LaTeX

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

Lean4

instance (J K : Precoverage C) [IsStableUnderSup J] [IsStableUnderSup K] : IsStableUnderSup (J ⊓ K) where
  sup_mem_coverings hR hS := ⟨J.sup_mem_coverings hR.1 hS.1, K.sup_mem_coverings hR.2 hS.2⟩

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