image₂_subset_iff_right — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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