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