mem_sep — Mathlib

English

Let p be a property on ZFSet. Then y is in the separation set sep p x if and only if y ∈ x and p(y).

Русский

Пусть p — свойство над ZFSet. Тогда y принадлежит сепаратору sep p x тогда и только тогда, когда y ∈ x и p(y).

LaTeX

$$$ y \in \mathrm{sep}(p,x) \iff y \in x \land p(y) $$$

Lean4

@[simp]
theorem mem_sep {p : ZFSet.{u} → Prop} {x y : ZFSet.{u}} : y ∈ ZFSet.sep p x ↔ y ∈ x ∧ p y :=
  Quotient.inductionOn₂ x y fun _ _ => PSet.mem_sep (p := p ∘ mk) fun _ _ h => (Quotient.sound h).subst

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