generate_of_contains_isSplitEpi — Mathlib

English

If a presieve contains a split epimorphism f, then generate R is the top sieve.

Русский

Если в пресеве содержится разложимый эпиморфизм f, то generate R = ⊤.

LaTeX

$$generate R = ⊤ if R f for IsSplitEpi f$$

Lean4

/-- If an arrow set contains a split epi, it generates the maximal sieve. -/
theorem generate_of_contains_isSplitEpi {R : Presieve X} (f : Y ⟶ X) [IsSplitEpi f] (hf : R f) : generate R = ⊤ :=
  by
  rw [← id_mem_iff_eq_top]
  exact ⟨_, section_ f, f, hf, by simp⟩

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