instIsStableUnderSupJointlySurjectivePrecoverage

English

JointlySurjectivePrecoverage is stable under taking sup (sum) of coverings: if R and S cover x, then there exists a combined covering.

Русский

JointlySurjectivePrecoverage устойчива к объединению охватов: если R и S покрывают x, то существует объединённый охват.

LaTeX

$$sup_mem_coverings {X} R S hR _ x$$

Lean4

instance : jointlySurjectivePrecoverage.IsStableUnderSup where
  sup_mem_coverings {X} R S hR _
    x := by
    obtain ⟨Y, f, hf, hx⟩ := hR x
    use Y, f, .inl hf

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