English
For a cone c over F, c is a limit if and only if for every section s ∈ F.sections there exists a unique x ∈ c.pt such that c.π.app j x = s(j) for all j.
Русский
Для конуса c над F конус является пределом тогда и только тогда, когда для каждой секции s ∈ F.sections существует единственный элемент x ∈ c.pt такой, что c.π.app j x = s(j) для всех j.
LaTeX
$$$\\text{Nonempty}(\\mathrm{IsLimit}(c)) \\iff \\forall s \\in F.\\mathrm{sections}, \\exists! x \\in c.pt, \\forall j, c.\\pi_{j}(x) = s(j).$$$
Lean4
theorem isLimit_iff (c : Cone F) : Nonempty (IsLimit c) ↔ ∀ s ∈ F.sections, ∃! x : c.pt, ∀ j, c.π.app j x = s j :=
by
refine ⟨fun ⟨t⟩ s hs ↦ ?_, fun h ↦ ⟨?_⟩⟩
· let cs := coneOfSection hs
exact
⟨t.lift cs ⟨⟩, fun j ↦ congr_fun (t.fac cs j) ⟨⟩, fun x hx ↦
congr_fun (t.uniq cs (fun _ ↦ x) fun j ↦ funext fun _ ↦ hx j) ⟨⟩⟩
· choose x hx using fun c y ↦ h _ (sectionOfCone c y).2
exact
⟨x, fun c j ↦ funext fun y ↦ (hx c y).1 j, fun c f hf ↦
funext fun y ↦ (hx c y).2 (f y) (fun j ↦ congr_fun (hf j) y)⟩
