English
For t ⊆ β, s ∈ f then s ∈ f ×ˢ principal t iff {a | ∀ b ∈ t, (a,b) ∈ s} ∈ f.
Русский
Для t ⊆ β верно: s ∈ f ×ˢ principal t тогда и только тогда, когда {a | ∀ b ∈ t, (a,b) ∈ s} ∈ f.
LaTeX
$$$s \\in f \\timesˢ \\mathfrak{p}t \\iff \\{a \\mid \\forall b \\in t, (a,b) \\in s\\} \\in f$$$
Lean4
@[simp]
theorem prod_mem_prod_iff [f.NeBot] [g.NeBot] : s ×ˢ t ∈ f ×ˢ g ↔ s ∈ f ∧ t ∈ g :=
⟨fun h =>
let ⟨_s', hs', _t', ht', H⟩ := mem_prod_iff.1 h
(prod_subset_prod_iff.1 H).elim (fun ⟨hs's, ht't⟩ => ⟨mem_of_superset hs' hs's, mem_of_superset ht' ht't⟩) fun h =>
h.elim (fun hs'e => absurd hs'e (nonempty_of_mem hs').ne_empty) fun ht'e =>
absurd ht'e (nonempty_of_mem ht').ne_empty,
fun h => prod_mem_prod h.1 h.2⟩
