Commit 2023-01-01 23:31 f668506a

View on Github →

feat: port Order.Closure (#1263) This made one change to a lemma statement to satisfy the linter. This change was also made in [mathlib#18024](https://github.com/leanprover-community/mathlib/pull/18024)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Order/Closure.lean

added def ClosureOperator.Simps.apply

added def ClosureOperator.closed

added theorem ClosureOperator.closed_eq_range_close

added theorem ClosureOperator.closure_eq_self_of_mem_closed

added theorem ClosureOperator.closure_inf_le

added theorem ClosureOperator.closure_is_closed

added theorem ClosureOperator.closure_le_closed_iff_le

added theorem ClosureOperator.closure_le_mk₃_iff

added theorem ClosureOperator.closure_mem_mk₃

added theorem ClosureOperator.closure_sup_closure

added theorem ClosureOperator.closure_sup_closure_le

added theorem ClosureOperator.closure_sup_closure_left

added theorem ClosureOperator.closure_sup_closure_right

added theorem ClosureOperator.closure_supᵢ_closure

added theorem ClosureOperator.closure_supᵢ₂_closure

added theorem ClosureOperator.closure_top

added theorem ClosureOperator.eq_mk₃_closed

added theorem ClosureOperator.ext

added def ClosureOperator.gi

added def ClosureOperator.id

added theorem ClosureOperator.idempotent

added theorem ClosureOperator.le_closure

added theorem ClosureOperator.le_closure_iff

added theorem ClosureOperator.mem_closed_iff

added theorem ClosureOperator.mem_closed_iff_closure_le

added theorem ClosureOperator.mem_mk₃_closed

added def ClosureOperator.mk'

added def ClosureOperator.mk₂

added def ClosureOperator.mk₃

added theorem ClosureOperator.monotone

added def ClosureOperator.toClosed

added theorem ClosureOperator.top_mem_closed

added structure ClosureOperator

added def GaloisConnection.closureOperator

added def GaloisConnection.lowerAdjoint

added def LowerAdjoint.Simps.apply

added def LowerAdjoint.closed

added theorem LowerAdjoint.closed_eq_range_close

added def LowerAdjoint.closureOperator

added theorem LowerAdjoint.closure_eq_self_of_mem_closed

added theorem LowerAdjoint.closure_inf_le

added theorem LowerAdjoint.closure_is_closed

added theorem LowerAdjoint.closure_le_closed_iff_le

added theorem LowerAdjoint.closure_sup_closure

added theorem LowerAdjoint.closure_sup_closure_le

added theorem LowerAdjoint.closure_sup_closure_left

added theorem LowerAdjoint.closure_sup_closure_right

added theorem LowerAdjoint.closure_supᵢ_closure

added theorem LowerAdjoint.closure_supᵢ₂_closure

added theorem LowerAdjoint.closure_top

added theorem LowerAdjoint.closure_union_closure

added theorem LowerAdjoint.closure_union_closure_left

added theorem LowerAdjoint.closure_union_closure_right

added theorem LowerAdjoint.closure_union_closure_subset

added theorem LowerAdjoint.closure_unionᵢ_closure

added theorem LowerAdjoint.closure_unionᵢ₂_closure

added theorem LowerAdjoint.eq_of_le

added theorem LowerAdjoint.ext

added theorem LowerAdjoint.gc

added theorem LowerAdjoint.idempotent

added theorem LowerAdjoint.le_closure

added theorem LowerAdjoint.le_closure_iff

added theorem LowerAdjoint.le_iff_subset

added theorem LowerAdjoint.mem_closed_iff

added theorem LowerAdjoint.mem_closed_iff_closure_le

added theorem LowerAdjoint.mem_iff

added theorem LowerAdjoint.monotone

added theorem LowerAdjoint.not_mem_of_not_mem_closure

added theorem LowerAdjoint.subset_closure

added def LowerAdjoint.toClosed

added structure LowerAdjoint

added theorem closureOperator_gi_self