liftOn_ofMem

Mathlib.Data.Semiquot

URI: https://scilib.ai/kg/mathlib#Semiquot.liftOn_ofMem

Lean4

theorem liftOn_ofMem (q : Semiquot α) (f : α → β) (h : ∀ a ∈ q, ∀ b ∈ q, f a = f b) (a : α) (aq : a ∈ q) :
    liftOn q f h = f a := by revert h; rw [eq_mk_of_mem aq]; intro; rfl

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru