image2

Mathlib.Data.Finite.Prod

URI: https://scilib.ai/kg/mathlib#Set.Finite.image2

← MathLib Explorer

English

If s and t are finite, then the image2 of f over s and t is finite.

Русский

Если s и t конечны, то image2 f s t конечен.

LaTeX

$$$ \forall f : \alpha \to \beta \to \gamma,\; s.Finite \land t.Finite \Rightarrow (image2\ f\ s\ t).Finite $$$

Lean4

protected theorem image2 (f : α → β → γ) (hs : s.Finite) (ht : t.Finite) : (image2 f s t).Finite :=
  by
  have := hs.to_subtype
  have := ht.to_subtype
  apply toFinite

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

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

Разделы

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

Аффилиация

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