image2_subset_iff

Mathlib.Data.Set.NAry

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

English

image2 f s t ⊆ u iff ∀ x ∈ s, ∀ y ∈ t, f x y ∈ u.

Русский

image2 f s t ⊆ u эквивалентно ∀ x ∈ s, ∀ y ∈ t, f x y ∈ u.

LaTeX

$$$image2 f s t ⊆ u \iff \forall x \in s, \forall y \in t, f x y ∈ u$$$

Lean4

@[simp]
theorem image2_subset_iff {u : Set γ} : image2 f s t ⊆ u ↔ ∀ x ∈ s, ∀ y ∈ t, f x y ∈ u :=
  forall_mem_image2

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

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

Разделы

Аффилиация

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