sep — Mathlib

English

The set {x ∈ s | t x} is equivalent to {x ∈ s | t x}, i.e., to {x : s | t x}.

Русский

Множество {x ∈ s | t x} эквивалентно {x : s | t x}.

LaTeX

$${x \in s \mid t(x)} \simeq {x : s | t x}$$

Lean4

/-- The set `{x ∈ s | t x}` is equivalent to the set of `x : s` such that `t x`. -/
protected def sep {α : Type u} (s : Set α) (t : α → Prop) : ({x ∈ s | t x} : Set α) ≃ {x : s | t x} :=
  (Equiv.subtypeSubtypeEquivSubtypeInter s t).symm

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