le_sInf — Mathlib

English

If every g ∈ s satisfies g ≤ f, then f is an upper bound for s, i.e., f ≥ sInf(s).

Русский

Если каждый g ∈ s удовлетворяет g ≤ f, то f является верхней границей для s, то есть f ≥ sInf(s).

LaTeX

$$f ≤ sInf(s)\n если \n ∀ g ∈ s, g ≤ f$$

Lean4

theorem le_sInf {A : C} (s : Set (Subobject A)) (f : Subobject A) (k : ∀ g ∈ s, f ≤ g) : f ≤ sInf s :=
  by
  fapply le_of_comm
  · exact Limits.limit.lift _ (leInfCone s f k) ≫ (underlyingIso _).inv
  · dsimp [sInf]
    rw [assoc, underlyingIso_arrow, widePullbackι, limit.lift_π, leInfCone_π_app_none]

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