sInf_le — Mathlib

English

If f ∈ s then sInf(s) ≤ f in the subobject order.

Русский

Если f принадлежит s, то sInf(s) ≤ f в порядке подпредметов.

LaTeX

$$sInf(s) \le f, \text{ если } f \in s$$

Lean4

theorem sInf_le {A : C} (s : Set (Subobject A)) (f) (hf : f ∈ s) : sInf s ≤ f :=
  by
  fapply le_of_comm
  ·
    exact
      (underlyingIso _).hom ≫
        Limits.limit.π (wideCospan s)
            (some ⟨equivShrink (Subobject A) f, Set.mem_image_of_mem (equivShrink (Subobject A)) hf⟩) ≫
          eqToHom (congr_arg (fun X : Subobject A => (X : C)) (Equiv.symm_apply_apply _ _))
  · dsimp [sInf]
    simp only [Category.assoc, ← underlyingIso_hom_comp_eq_mk, Iso.cancel_iso_hom_left]
    convert limit.w (wideCospan s) (WidePullbackShape.Hom.term _)
    simp

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