seq_subset — Mathlib

English

For sets s of functions, t ⊆ α, and u ⊆ γ, seq s t ⊆ u iff for every f ∈ s and a ∈ t, f(a) ∈ u.

Русский

Для множеств функций s, t ⊆ α, u ⊆ γ верно: seq s t ⊆ u тогда, когда для каждого f ∈ s и a ∈ t верно f(a) ∈ u.

LaTeX

$$$$ \\operatorname{seq} s t \\subseteq u \\;\\Longleftrightarrow\\; \\forall f \\in s, \\forall a \\in t, f(a) \\in u $$$$

Lean4

theorem seq_subset {s : Set (α → β)} {t : Set α} {u : Set β} : seq s t ⊆ u ↔ ∀ f ∈ s, ∀ a ∈ t, (f : α → β) a ∈ u :=
  image2_subset_iff

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