map' — Mathlib

English

The map' construction assigns to a morphism f and element x the least element in a specific finite set determined by f and x.

Русский

Конструкция map' назначает наименьший элемент из конечного множества, определённого f и x.

LaTeX

$$$map'(f,x) = \min' (finset f x) (nonempty\_finset f x).$$$

Lean4

/-- Auxiliary definition for the definition of the action of the
functor `SimplexCategory.II` on morphisms. -/
def map' (f : Fin (n + 1) →o Fin (m + 1)) (x : Fin (m + 2)) : Fin (n + 2) :=
  (finset f x).min' (nonempty_finset f x)

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