eventually_curry_prod_iff — Mathlib

English

If l and m are nonempty filters and s ⊆ α, t ⊆ β, then eventually x in l.curry m lies in s × t if and only if s ∈ l and t ∈ m.

Русский

Если l и m ненулевые фильтры и s ⊆ α, t ⊆ β, то в итоге x в l.curry m принадлежит s × t тогда и только тогда, когда s ∈ l и t ∈ m.

LaTeX

$$$[l,m]\text{ NeBot} \Rightarrow (\forall s,t, (\forall^\infty x \in l.curry m, x ∈ s\times t) \iff s ∈ l ∧ t ∈ m)$$

Lean4

theorem eventually_curry_prod_iff [NeBot l] [NeBot m] : (∀ᶠ x in l.curry m, x ∈ s ×ˢ t) ↔ s ∈ l ∧ t ∈ m := by
  simp [eventually_curry_iff]

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