le_seq — Mathlib

English

If for every t ∈ f and u ∈ g, t.seq u ∈ h, then h ≤ f.seq g.

Русский

Если для всех t ∈ f и u ∈ g верно t.seq u ∈ h, то h ⊆ f.seq g.

LaTeX

$$$ \forall t \in f, \forall u \in g, t \text{.seq} u \in h \;\Rightarrow\; h \le f \text{.seq } g $$$

Lean4

theorem le_seq {f : Filter (α → β)} {g : Filter α} {h : Filter β} (hh : ∀ t ∈ f, ∀ u ∈ g, Set.seq t u ∈ h) :
    h ≤ seq f g := fun _ ⟨_, ht, _, hu, hs⟩ =>
  mem_of_superset (hh _ ht _ hu) fun _ ⟨_, hm, _, ha, eq⟩ => eq ▸ hs _ hm _ ha

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