instSetLike — Mathlib

English

Two filters on P are equal precisely when their underlying sets (as subsets of P) are equal.

Русский

Два фильтра на P тождественны тогда и только тогда, когда их подмножества множества P совпадают.

LaTeX

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

Lean4

/-- A filter on `P` is a subset of `P`. -/
instance : SetLike (PFilter P) P where
  coe F := toDual ⁻¹' F.dual.carrier
  coe_injective' := fun ⟨_⟩ ⟨_⟩ h => congr_arg mk <| Ideal.ext h

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