sSup_le — Mathlib

English

The supremum of a set s of subobjects is the subobject given by the image of smallCoproductDesc s.

Русский

Супремум множества подпредметов s есть подпредмет, задаваемый как образ coproduct через smallCoproductDesc.

LaTeX

$$sSup s = Subobject.mk (image.ι (smallCoproductDesc s))$$

Lean4

theorem sSup_le {A : C} (s : Set (Subobject A)) (f : Subobject A) (k : ∀ g ∈ s, g ≤ f) : sSup s ≤ f :=
  by
  fapply le_of_comm
  · refine (underlyingIso _).hom ≫ image.lift ⟨_, f.arrow, ?_, ?_⟩
    · refine Sigma.desc ?_
      rintro ⟨g, m⟩
      refine underlying.map (homOfLE (k _ ?_))
      simpa using m
    · ext
      dsimp [smallCoproductDesc]
      simp
  · dsimp [sSup]
    rw [assoc, image.lift_fac, underlyingIso_hom_comp_eq_mk]

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