small_image2

Mathlib.Logic.Small.Set

URI: https://scilib.ai/kg/mathlib#small_image2

← MathLib Explorer

English

If s and t are Small, then Set.image2 f s t is Small.

Русский

Если s и t малы, то Set.image2 f s t мала.

LaTeX

$$$Small(s) \Rightarrow Small(t) \Rightarrow Small(Set.image2\ f\ s\ t).$$$

Lean4

instance small_image2 (f : α → β → γ) (s : Set α) (t : Set β) [Small.{u} s] [Small.{u} t] :
    Small.{u} (Set.image2 f s t) := by
  rw [← Set.image_uncurry_prod]
  infer_instance

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

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

Разделы

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

Аффилиация

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