mem_prod_principal — Mathlib

English

Variant formulation for mem_prod_principal with explicit t and x,y expansions.

Русский

Вариант формулировки mem_prod_principal с явным развертыванием по x,y.

LaTeX

$$$s \\in f ×ˢ 𝓟 t \\iff \\{a \\mid ∀ b \\in t, (a,b) ∈ s\\} ∈ f$$$

Lean4

theorem mem_prod_principal {s : Set (α × β)} : s ∈ f ×ˢ 𝓟 t ↔ {a | ∀ b ∈ t, (a, b) ∈ s} ∈ f :=
  by
  rw [← @exists_mem_subset_iff _ f, mem_prod_iff]
  refine exists_congr fun u => Iff.rfl.and ⟨?_, fun h => ⟨t, mem_principal_self t, ?_⟩⟩
  · rintro ⟨v, v_in, hv⟩ a a_in b b_in
    exact hv (mk_mem_prod a_in <| v_in b_in)
  · rintro ⟨x, y⟩ ⟨hx, hy⟩
    exact h hx y hy

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