image₂_left

Mathlib.Data.Finset.NAry

URI: https://scilib.ai/kg/mathlib#Finset.image₂_left

← MathLib Explorer

English

If t is nonempty, then image₂ (fun x _ => x) s t = s.

Русский

Если t непусто, то image₂ (id, правой части) образует s: image₂ (fun x _ => x) s t = s.

LaTeX

$$$t.Nonempty \Rightarrow \mathrm{image}_2\ (\lambda x. x)\ s\ t = s$$$

Lean4

@[simp]
theorem image₂_left [DecidableEq α] (h : t.Nonempty) : image₂ (fun x _ => x) s t = s :=
  coe_injective <| by
    push_cast
    exact image2_left h

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

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

Разделы

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

Аффилиация

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