curry — Mathlib

English

The curry operation preserves the CountableInterFilter structure: the curry of l and m is CountableInterFilter.

Русский

Операция карри сохраняет структуру CountableInterFilter.

LaTeX

$$$\\text{curry} : CountableInterFilter l \\to CountableInterFilter m \\Rightarrow \\text{curry}(l,m) \\text{ is CountableInterFilter}$$$

Lean4

instance curry {α β : Type*} {l : Filter α} {m : Filter β} [CountableInterFilter l] [CountableInterFilter m] :
    CountableInterFilter (l.curry m) :=
  ⟨by
    intro S Sct hS
    simp_rw [mem_curry_iff, mem_sInter, eventually_countable_ball (p := fun _ _ _ => (_, _) ∈ _) Sct,
      eventually_countable_ball (p := fun _ _ _ => ∀ᶠ (_ : β) in m, _) Sct, ← mem_curry_iff]
    exact hS⟩

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