seq_mono — Mathlib

English

If s0 ⊆ s1 and t0 ⊆ t1 then seq s0 t0 ⊆ seq s1 t1; i.e., the seq operation is monotone in both arguments.

Русский

Если s0 ⊆ s1 и t0 ⊆ t1, то seq s0 t0 ⊆ seq s1 t1; то есть операция seq монотонна по обеим аргументам.

LaTeX

$$$$ \\text{seq}(s_0,t_0) \\subseteq \\text{seq}(s_1,t_1) $$$$

Lean4

@[gcongr, mono]
theorem seq_mono {s₀ s₁ : Set (α → β)} {t₀ t₁ : Set α} (hs : s₀ ⊆ s₁) (ht : t₀ ⊆ t₁) : seq s₀ t₀ ⊆ seq s₁ t₁ :=
  image2_subset hs ht

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