Theorems · Theorem · order theory
ClosureOperator.isClosed_iff
∀ {α : Type u_1} [inst : Preorder α] (self : ClosureOperator α) {x : α}, self.IsClosed x ↔ self.toFun x = x- Defined in
- Mathlib.Order.Closure
- Cited by
- 14 results in Mathlib
- Foundations
- Depth 3 from the axioms · uses no axioms
- Assumes
- Preorder
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Preorderstatement and proof · cited by 7,952
- ClosureOperatorstatement and proof · cited by 371
- OrderHom.toFunstatement · cited by 45
- ClosureOperator.IsClosedstatement · cited by 38
- ClosureOperator.toOrderHomstatement · cited by 6
Cited by14
Results whose statement or proof uses this declaration.
- ClosureOperator.isClosed_closureproof · cited by 15
- countableInfClosure_eq_selfproof · cited by 4
- infClosure_eq_selfproof · cited by 4
- ClosureOperator.IsClosed.closure_eqproof · cited by 3
- ClosureOperator.isClosed_iff_closure_leproof · cited by 3
- convexHull_eq_selfproof · cited by 2
- CategoryTheory.GrothendieckTopology.isClosed_iff_close_eq_selfproof · cited by 1
- latticeClosure_eq_selfproof · cited by 1
- supClosure_eq_selfproof · cited by 1
- Convexity.convexHull_eq_selfproof · cited by 1
- absConvexHull_eq_selfproof · cited by 1
- countableSupClosure_eq_selfproof · cited by 1