obj — Mathlib

English

The map Mk₁.obj gives a function Fin 2 → C selecting the left or right input for a pair (X₀, X₁).

Русский

Функция Mk₁.obj выбирает между двумя входами пары (X₀, X₁) по индексу Fin 2.

LaTeX

$${ obj : Fin 2 → C, obj ⟨0, _⟩ = X₀, obj ⟨1, _⟩ = X₁ }$$

Lean4

/-- The map which sends `0 : Fin 2` to `X₀` and `1` to `X₁`. -/
@[simp]
def obj : Fin 2 → C
  | ⟨0, _⟩ => X₀
  | ⟨1, _⟩ => X₁

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