ext_isClosed — Mathlib

English

If two closure operators have the same closed elements, then they are equal.

Русский

Если два замыкателя имеют одинаковые замкнутые элементы, то они равны между собой.

LaTeX

$$$\\\\forall {\\\\alpha : Type*} [PartialOrder {\\\\alpha}] (c_1 c_2 : ClosureOperator {\\\\alpha}), \\\\forall x, c_1.IsClosed x \\\\leftrightarrow c_2.IsClosed x \\\\Rightarrow c_1 = c_2$$$

Lean4

theorem ext_isClosed (c₁ c₂ : ClosureOperator α) (h : ∀ x, c₁.IsClosed x ↔ c₂.IsClosed x) : c₁ = c₂ :=
  ext c₁ c₂ <| fun x =>
    IsGLB.unique (c₁.closure_isGLB x) <| (Set.ext (and_congr_right' <| h ·)).substr (c₂.closure_isGLB x)

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