fiberInclusion_comp_eq_const — Mathlib

English

The composite fiberInclusion followed by p is the constant functor to S; i.e., fiberInclusion ⋙ p = (const (Fiber p S)).obj S.

Русский

Состав fiberInclusion и затем p равен константному функтору в S; fiberInclusion ⋙ p = (const (Fiber p S)).obj S.

LaTeX

$$$\\text{fiberInclusion} \\;\\!\\!\\!\\; \\!\\!\\!\\; p = (\\text{const } (\\text{Fiber } p S)).\\text{obj } S$$$

Lean4

theorem fiberInclusion_comp_eq_const : fiberInclusion ⋙ p = (const (Fiber p S)).obj S :=
  Functor.ext_of_iso fiberInclusionCompIsoConst (fun x ↦ x.2)

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