ext — Mathlib

English

A PFilter is determined by its underlying subset: equals iff the carriers are equal.

Русский

Фильтр на P задаётся своим подмножеством: равен тогда и только тогда, когда их носители совпадают.

LaTeX

$$$$ s = t \\iff (s : Set P) = (t : Set P). $$$$

Lean4

/-- Two filters are equal when their underlying sets are equal. -/
@[ext]
theorem ext (h : (s : Set P) = t) : s = t :=
  SetLike.ext' h

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