English
The map' construction assigns to a morphism f: Fin(n+1) → Fin(m+1) and x ∈ Fin(m+2) the least element in an associated finite set of Fin(n+2) determined by f and x.
Русский
Конструкция map' для морфизма f и элемента x выбирает наименьший элемент в соответствующем конечном множестве Fin(n+2), задаваемом f и x.
LaTeX
$$$map'(f,x) = \min' (finset\ f\ x)\, (nonempty\_finset\ f\ x).$$$
Lean4
/-- Auxiliary definition for `map'`. Given `f : Fin (n + 1) →o Fin (m + 1)` and
`x : Fin (m + 2)`, `map' f x` shall be the smallest element in
this `finset f x : Finset (Fin (n + 2))`. -/
def finset (f : Fin (n + 1) →o Fin (m + 1)) (x : Fin (m + 2)) : Finset (Fin (n + 2)) :=
Finset.univ.filter (fun i ↦ i = Fin.last _ ∨ ∃ (h : i ≠ Fin.last _), x ≤ (f (i.castPred h)).castSucc)
