closureOperator_gi_self — Mathlib

English

For a closure operator c, the associated Galois insertion recovers c from its GC: c.gi.gc.closureOperator = c.

Русский

Для замыкательного оператора c соответствующая вставка Галуа восстанавливает его: c.gi.gc.closureOperator = c.

LaTeX

$$$c.gi.gc.closureOperator = c$$$

Lean4

/-- The Galois insertion associated to a closure operator can be used to reconstruct the closure
operator.
Note that the inverse in the opposite direction does not hold in general. -/
@[simp]
theorem closureOperator_gi_self [PartialOrder α] (c : ClosureOperator α) : c.gi.gc.closureOperator = c :=
  by
  ext x
  rfl

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