mem_seq_def — Mathlib

English

Let f be a filter on (α → β), g a filter on α, and s a subset of β. Then s ∈ f.seq g if and only if there exist u ∈ f and t ∈ g such that ∀ x ∈ u, ∀ y ∈ t, x(y) ∈ s.

Русский

Пусть f — фильтр на (α → β), g — фильтр на α, и s ⊆ β. Тогда s ∈ f.seq g тогда, когда найдутся u ∈ f и t ∈ g такие, что ∀ x ∈ u, ∀ y ∈ t, x(y) ∈ s.

LaTeX

$$$ s \in f.seq g \iff \exists u \in f, \exists t \in g, \forall x \in u, \forall y \in t, x(y) \in s $$$

Lean4

theorem mem_seq_def {f : Filter (α → β)} {g : Filter α} {s : Set β} :
    s ∈ f.seq g ↔ ∃ u ∈ f, ∃ t ∈ g, ∀ x ∈ u, ∀ y ∈ t, (x : α → β) y ∈ s :=
  Iff.rfl

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