leInfCone — Mathlib

English

Auxiliary construction: leInfCone(s) provides a cone on the wideCospan(s) with apex f, whose legs are given by the maps k to each g in s.

Русский

Вспомогательное построение: leInfCone(s) образует кону над wideCospan(s) с вершиной в f, а рёбра задаются отображениями k к каждому g в s.

LaTeX

$$def leInfCone {A : C} (s : Set (Subobject A)) (f : Subobject A) (k : ∀ g ∈ s, f ≤ g) : Cone (wideCospan s)$$

Lean4

/-- Auxiliary construction of a cone for `le_inf`. -/
def leInfCone {A : C} (s : Set (Subobject A)) (f : Subobject A) (k : ∀ g ∈ s, f ≤ g) : Cone (wideCospan s) :=
  WidePullbackShape.mkCone f.arrow
    (fun j =>
      underlying.map
        (homOfLE
          (k _
            (by
              rcases j with ⟨-, ⟨g, ⟨m, rfl⟩⟩⟩
              simpa using m))))
    (by simp)

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