eq_ofPred_closed — Mathlib

English

A closure operator is determined by the predicate 'x is closed'; the closure operator can be reconstructed from this predicate.

Русский

Замыкатель определяется предикатом «x замкнуто»; замыкатель можно восстановить по этому предикату.

LaTeX

$$$c = \\operatorname{ofPred}(c, c.IsClosed, c.le_closure, c.isClosed_closure, (\\\\lambda _ _ , closure_min))$$$

Lean4

/-- A closure operator is equal to the closure operator obtained by feeding `c.closed` into the
`ofPred` constructor. -/
theorem eq_ofPred_closed (c : ClosureOperator α) :
    c = ofPred c c.IsClosed c.le_closure c.isClosed_closure fun _ _ ↦ closure_min :=
  by
  ext
  rfl

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