ofSection_eq_range' — Mathlib

English

If X is an object of Cᵒᵖ, then ofSection x equals the range of uliftYonedaEquiv symm applied to x.

Русский

Если X — объект Cᵒᵖ, то ofSection x равен диапазону uliftYonedaEquiv.symm примененной к x.

LaTeX

$$$ ofSection x = range (yonedaEquiv.symm\\ x) $$$

Lean4

theorem ofSection_eq_range' {X : Cᵒᵖ} (x : F.obj X) : ofSection x = range (uliftYonedaEquiv.symm x) :=
  by
  ext U y
  dsimp [uliftYonedaEquiv]
  simp only [Set.mem_range, ULift.exists]
  constructor
  · rintro ⟨f, rfl⟩
    exact ⟨f.unop, rfl⟩
  · rintro ⟨f, rfl⟩
    exact ⟨f.op, rfl⟩

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