mk_sep — Mathlib

English

The cardinality of the subset {x ∈ s | t x} equals the cardinality of the corresponding subtype {x ∈ s | t x.1}.

Русский

Кардинал множества {x ∈ s | t x} равен кардиналу соответствующего подвида {x ∈ s | t x.1}.

LaTeX

$$$\\#\\{x \\in s \\mid t\,x\\} = \\#\\{x : s \\mid t\\,x.1\\}$$$

Lean4

theorem mk_sep (s : Set α) (t : α → Prop) : #({x ∈ s | t x} : Set α) = #{x : s | t x.1} :=
  mk_congr (Equiv.Set.sep s t)

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