mem_pairSep — Mathlib

English

z ∈ pairSep p x y iff ∃ a ∈ x, ∃ b ∈ y, z = pair a b ∧ p a b.

Русский

z ∈ pairSep p x y тогда и только тогда, когда найдётся a ∈ x и b ∈ y такие, что z = pair a b и p a b.

LaTeX

$$$z \\in \\mathrm{pairSep}\\ p\\ x\\ y \\iff \\exists a \\in x, \\exists b \\in y, z = a.pair b \\land p a b$$$

Lean4

@[simp]
theorem mem_pairSep {p} {x y z : ZFSet.{u}} : z ∈ pairSep p x y ↔ ∃ a ∈ x, ∃ b ∈ y, z = pair a b ∧ p a b :=
  by
  refine mem_sep.trans ⟨And.right, fun e => ⟨?_, e⟩⟩
  grind [mem_pair, mem_powerset, mem_singleton, mem_union, pair, subset_def]

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