mem_image₂_of_mem

Mathlib.Data.Finset.NAry

URI: https://scilib.ai/kg/mathlib#Finset.mem_image₂_of_mem

English

If a ∈ s and b ∈ t, then f a b ∈ image₂ f s t.

Русский

Если a ∈ S и b ∈ T, то f a b ∈ image₂ f S T.

LaTeX

$$mem_image₂_of_mem (ha : a ∈ s) (hb : b ∈ t) : f a b ∈ image₂ f s t$$

Lean4

theorem mem_image₂_of_mem (ha : a ∈ s) (hb : b ∈ t) : f a b ∈ image₂ f s t :=
  mem_image₂.2 ⟨a, ha, b, hb, rfl⟩

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

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

Разделы

Аффилиация

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