image_inf_prod

Mathlib.Data.Set.Sups

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

English

The image of the product map (x, y) ↦ x ⊓ y over S × T equals the infimum set S ⊼ T.

Русский

Образ отображения (x, y) ↦ x ⊓ y над S × T равен множеству инфимумов S ⊼ T.

LaTeX

$$$\\mathrm{image2} (\\lambda x\\ x'\\mapsto x \\wedge x')\n s\\ t = s \\⊼ t$$

Lean4

@[simp]
theorem image_inf_prod (s t : Set α) : Set.image2 (fun x x_1 => x ⊓ x_1) s t = s ⊼ t :=
  rfl

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

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

Разделы

Аффилиация

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