instIsCoverDense — Mathlib

English

There is a canonical isomorphism between P⁺ ⋙ F and (P ⋙ F)⁺.

Русский

Существет каноническое изоморфизм между P⁺ ⋙ F и (P ⋙ F)⁺.

LaTeX

$$$(J.\\text{plusObj } P) \\;\\circ F \\;\\cong\\; J.\\text{plusObj } (P \\circ F)$$$

Lean4

instance : F.IsCoverDense (regularTopology _) :=
  by
  refine F.isCoverDense_of_generate_singleton_functor_π_mem _ fun B ↦ ⟨_, F.effectiveEpiOver B, ?_⟩
  apply Coverage.Saturate.of
  refine ⟨F.effectiveEpiOverObj B, F.effectiveEpiOver B, ?_, inferInstance⟩
  funext;
  ext -- Do we want `Presieve.ext`?

  refine ⟨fun ⟨⟩ ↦ ⟨()⟩, ?_⟩
  rintro ⟨⟩
  simp

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