mem_sep — Mathlib

English

Membership in the separator PSet.sep p x is equivalent to y ∈ x and p y, provided p is invariant under equivalence.

Русский

Членство в сепараторе PSet.sep p x эквивалентно y ∈ x и p(y), при условии инвариантности p по отношению эквивалентности.

LaTeX

$$$ (\\\\forall x y : PSet),\\\\ (y \\\\in PSet.sep p x) \\\\leftrightarrow (y \\\\in x \\\\and p y)$$$

Lean4

theorem mem_sep {p : PSet → Prop} (H : ∀ x y, Equiv x y → p x → p y) : ∀ {x y : PSet}, y ∈ PSet.sep p x ↔ y ∈ x ∧ p y
  | ⟨_, _⟩, _ => ⟨fun ⟨⟨a, pa⟩, h⟩ => ⟨⟨a, h⟩, H _ _ h.symm pa⟩, fun ⟨⟨a, h⟩, pa⟩ => ⟨⟨a, H _ _ h pa⟩, h⟩⟩

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