mem_prod_top — Mathlib

English

Membership in f ×ˢ ⊤ equals the condition that a's with all b satisfy (a,b) ∈ s.

Русский

Принадлежность в f ×ˢ ⊤ равна условию: множество a таких, что для всех b, (a,b) удовлетворяет s.

LaTeX

$$$s \\in f \\timesˢ \\top \\iff {a | ∀ b, (a,b) ∈ s} ∈ f$$$

Lean4

theorem mem_prod_top {s : Set (α × β)} : s ∈ f ×ˢ (⊤ : Filter β) ↔ {a | ∀ b, (a, b) ∈ s} ∈ f :=
  by
  rw [← principal_univ, mem_prod_principal]
  simp only [mem_univ, forall_true_left]

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