image₂_subset_iff_left — Mathlib

English

Let f : α → β → γ, s ⊆ α, t ⊆ β, u ⊆ γ. Then image₂ f s t ⊆ u iff for every a ∈ s the set (t.image (f a ·)) is contained in u.

Русский

Пусть f : α → β → γ, s ⊆ α, t ⊆ β, u ⊆ γ. Тогда image₂ f s t ⊆ u эквивалентно тому, что для каждого a ∈ s множество {f(a,b) | b ∈ t} ⊆ u.

LaTeX

$$$\\operatorname{image}_2 f\, s\, t \\subseteq u \\iff \\forall a \\in s, (t.\\operatorname{image} (\\lambda b. f\, a\, b)) \\subseteq u$$$

Lean4

theorem image₂_subset_iff_left : image₂ f s t ⊆ u ↔ ∀ a ∈ s, (t.image fun b => f a b) ⊆ u := by
  simp_rw [image₂_subset_iff, image_subset_iff]

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