le_sSup — Mathlib

English

If every g ∈ s satisfies g ≤ f, then sSup(s) ≤ f.

Русский

Если каждый g ∈ s удовлетворяет g ≤ f, тогда sSup(s) ≤ f.

LaTeX

$$∀ g ∈ s, g ≤ f → sSup(s) ≤ f$$

Lean4

theorem le_sSup {A : C} (s : Set (Subobject A)) (f) (hf : f ∈ s) : f ≤ sSup s :=
  by
  fapply le_of_comm
  · refine
      eqToHom ?_ ≫
        Sigma.ι _ ⟨equivShrink (Subobject A) f, by simpa [Set.mem_image] using hf⟩ ≫
          factorThruImage _ ≫ (underlyingIso _).inv
    exact (congr_arg (fun X : Subobject A => (X : C)) (Equiv.symm_apply_apply _ _).symm)
  · simp [sSup, smallCoproductDesc]

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