canLift — Mathlib

English

There is a lifting from a function on the ambient type to a function on the Finset's elements, via the canonical embedding that sends a to the pair ⟨a, a ∈ s⟩.

Русский

Существует подъем от функции на окружающий тип к функции на элементах Finset через каноническое вложение, которое отправляет a в пару ⟨a, a ∈ s⟩.

LaTeX

$$CanLift (s : Finset α) : CanLift α s (↑) (fun a => a ∈ s)$$

Lean4

instance canLift (s : Finset α) : CanLift α s (↑) fun a => a ∈ s where prf a ha := ⟨⟨a, ha⟩, rfl⟩

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