image_prod

Mathlib.Data.Set.NAry

URI: https://scilib.ai/kg/mathlib#Set.image_prod

English

A symmetric formulation of image2 subset: Iff between subset of image2 and pointwise membership.

Русский

Симметричное формулирование подмножества image2 через явления по координатам.

LaTeX

$$Iff (image2 f s t ⊆ u) (∀ b ∈ t, (f · b) '' s ⊆ u).$$

Lean4

@[simp]
theorem image_prod : (fun x : α × β ↦ f x.1 x.2) '' s ×ˢ t = image2 f s t :=
  ext fun _ ↦ by simp [and_assoc]

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

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

Разделы

Аффилиация

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