Grace/Cumulus/Lattice/Monotone.g17

Open in Workbench Download source

Imports

Complete

Declarations

Source

1-- Monotone maps between ordered sets, Galois connections, and closure2-- operators3-- Part of Cumulus, the Grace17 mathematics library.4-- Copyright (c) 2026 Grant Passmore.5-- Released under the Apache License 2.0. See LICENSE in the repository root.6-- Authors: Grant Passmore78module Grace.Cumulus.Lattice.Monotone9import Complete1011predicate IsMonotoneMap (f A r B s : Set) :=12  FunctionBetween(f, A, B) ∧13  (∀ x ∈ A, ∀ y ∈ A, relates(r, x, y) → relates(s, f(x), f(y)))1415predicate IsAntitoneMap (f A r B s : Set) :=16  FunctionBetween(f, A, B) ∧17  (∀ x ∈ A, ∀ y ∈ A, relates(r, x, y) → relates(s, f(y), f(x)))1819-- A Galois connection: f is left adjoint to g.20predicate IsGaloisConnection (f A r g B s : Set) :=21  FunctionBetween(f, A, B) ∧ FunctionBetween(g, B, A) ∧22  (∀ x ∈ A, ∀ y ∈ B, (relates(s, f(x), y) ↔ relates(r, x, g(y))))2324predicate IsClosureOperator (c A r : Set) :=25  FunctionBetween(c, A, A) ∧26  (∀ x ∈ A, relates(r, x, c(x))) ∧27  (∀ x ∈ A, ∀ y ∈ A, relates(r, x, y) → relates(r, c(x), c(y))) ∧28  (∀ x ∈ A, c(c(x)) = c(x))2930-- Monotone maps3132theorem IsMonotoneMap.function (f A r B s : Set)33  requires h : IsMonotoneMap(f, A, r, B, s)34  shows f : A → B35proof36  simp [IsMonotoneMap]3738theorem IsMonotoneMap.preserves (f A r B s x y : Set)39  requires h : IsMonotoneMap(f, A, r, B, s)40  requires hx : x ∈ A41  requires hy : y ∈ A42  requires hxy : relates(r, x, y)43  shows relates(s, f(x), f(y))44proof45  rcases h with ⟨function, monotone⟩46  exact monotone with x, hx, y, hy, hxy4748theorem IsMonotoneMap.apply_member (f A r B s x : Set)49  requires h : IsMonotoneMap(f, A, r, B, s)50  requires hx : x ∈ A51  shows f(x) ∈ B52proof53  exact FunctionBetween.apply_closed with (IsMonotoneMap.function with h), hx5455theorem IsAntitoneMap.function (f A r B s : Set)56  requires h : IsAntitoneMap(f, A, r, B, s)57  shows f : A → B58proof59  simp [IsAntitoneMap]6061theorem IsAntitoneMap.reverses (f A r B s x y : Set)62  requires h : IsAntitoneMap(f, A, r, B, s)63  requires hx : x ∈ A64  requires hy : y ∈ A65  requires hxy : relates(r, x, y)66  shows relates(s, f(y), f(x))67proof68  rcases h with ⟨function, antitone⟩69  exact antitone with x, hx, y, hy, hxy7071theorem IsMonotoneMap.identity (A r : Set)72  shows IsMonotoneMap(identity(A), A, r, A, r)73proof74  constructor75  . exact identity.function at A76  . intros x hx y hy hxy77    have valueX := identity.apply with hx78    have valueY := identity.apply with hy79    rw [valueX, valueY]80    exact hxy8182theorem IsMonotoneMap.compose (f g A r B s C t : Set)83  requires hf : IsMonotoneMap(f, A, r, B, s)84  requires hg : IsMonotoneMap(g, B, s, C, t)85  shows IsMonotoneMap(compose(g, f, A, B, C), A, r, C, t)86proof87  have fFunction := IsMonotoneMap.function with hf88  have gFunction := IsMonotoneMap.function with hg89  constructor90  . exact compose.function with fFunction, gFunction91  . intros x hx y hy hxy92    have valueX := compose.apply with fFunction, gFunction, hx93    have valueY := compose.apply with fFunction, gFunction, hy94    rw [valueX, valueY]95    have fxB := FunctionBetween.apply_closed with fFunction, hx96    have fyB := FunctionBetween.apply_closed with fFunction, hy97    have mapped := IsMonotoneMap.preserves with hf, hx, hy, hxy98    exact IsMonotoneMap.preserves with hg, fxB, fyB, mapped99100theorem IsMonotoneMap.converse (f A r B s : Set)101  requires h : IsMonotoneMap(f, A, r, B, s)102  shows IsMonotoneMap(f, A, converse(r, A, A), B, converse(s, B, B))103proof104  have function := IsMonotoneMap.function with h105  constructor106  . exact function107  . intros x hx y hy hxy108    have yx := converse.reflects with hxy109    have mapped := IsMonotoneMap.preserves with h, hy, hx, yx110    have fxB := FunctionBetween.apply_closed with function, hx111    have fyB := FunctionBetween.apply_closed with function, hy112    exact converse.relates with fyB, fxB, mapped113114theorem IsAntitoneMap.monotone_converse (f A r B s : Set)115  requires h : IsAntitoneMap(f, A, r, B, s)116  shows IsMonotoneMap(f, A, r, B, converse(s, B, B))117proof118  have function := IsAntitoneMap.function with h119  constructor120  . exact function121  . intros x hx y hy hxy122    have reversed := IsAntitoneMap.reverses with h, hx, hy, hxy123    have fxB := FunctionBetween.apply_closed with function, hx124    have fyB := FunctionBetween.apply_closed with function, hy125    exact converse.relates with fyB, fxB, reversed126127theorem OrderEmbedding.monotone (f A r B s : Set)128  requires h : OrderEmbedding(f, A, r, B, s)129  shows IsMonotoneMap(f, A, r, B, s)130proof131  rcases h with ⟨injective, ordered⟩132  have function := Injective.function with injective133  constructor134  . exact function135  . intros x hx y hy hxy136    have fxB := FunctionBetween.apply_closed with function, hx137    have fyB := FunctionBetween.apply_closed with function, hy138    have mapX := FunctionBetween.relates_apply with function, hx139    have mapY := FunctionBetween.relates_apply with function, hy140    have preserved := ordered with x, hx, y, hy, f(x), fxB, f(y), fyB, mapX,141        mapY142    exact preserved.forward with hxy143144theorem OrderEmbedding.reflects (f A r B s x y : Set)145  requires h : OrderEmbedding(f, A, r, B, s)146  requires hx : x ∈ A147  requires hy : y ∈ A148  requires hxy : relates(s, f(x), f(y))149  shows relates(r, x, y)150proof151  rcases h with ⟨injective, ordered⟩152  have function := Injective.function with injective153  have fxB := FunctionBetween.apply_closed with function, hx154  have fyB := FunctionBetween.apply_closed with function, hy155  have mapX := FunctionBetween.relates_apply with function, hx156  have mapY := FunctionBetween.relates_apply with function, hy157  have preserved := ordered with x, hx, y, hy, f(x), fxB, f(y), fyB, mapX, mapY158  exact preserved.backward with hxy159160theorem OrderIsomorphism.monotone (f A r B s : Set)161  requires h : OrderIsomorphism(f, A, r, B, s)162  shows IsMonotoneMap(f, A, r, B, s)163proof164  exact OrderEmbedding.monotone with (OrderIsomorphism.embedding with h)165166-- Chains and bounds under a monotone map167168theorem IsMonotoneMap.chain (f A r B s C : Set)169  requires h : IsMonotoneMap(f, A, r, B, s)170  requires chain : Chain(A, r, C)171  shows Chain(B, s, functionImage(f, C, B))172proof173  rcases chain with ⟨bounded, comparable⟩174  constructor175  . exact functionImage.subset at f, C, B176  . intros u hu v hv177    obtain ⟨uB, x, hx, rfl⟩ := functionImage.membership.forward with hu178    obtain ⟨vB, y, hy, rfl⟩ := functionImage.membership.forward with hv179    have xA := bounded with x, hx180    have yA := bounded with y, hy181    have cases := comparable with x, hx, y, hy182    cases cases with xy | yx183    . left184      exact IsMonotoneMap.preserves with h, xA, yA, xy185    . right186      exact IsMonotoneMap.preserves with h, yA, xA, yx187188theorem IsMonotoneMap.image_upper (f A r B s S u : Set)189  requires h : IsMonotoneMap(f, A, r, B, s)190  requires bound : UpperBound(A, r, S, u)191  shows UpperBound(B, s, functionImage(f, S, B), f(u))192proof193  have uA := UpperBound.member with bound194  have bounded := UpperBound.subset with bound195  refine ⟨(IsMonotoneMap.apply_member with h, uA), (functionImage.subset at f,196      S, B), ?_⟩197  intros v hv198  obtain ⟨vB, x, hx, rfl⟩ := functionImage.membership.forward with hv199  have above := UpperBound.above with bound, hx200  exact IsMonotoneMap.preserves with h, (bounded with x, hx), uA, above201202theorem IsMonotoneMap.image_lower (f A r B s S l : Set)203  requires h : IsMonotoneMap(f, A, r, B, s)204  requires bound : LowerBound(A, r, S, l)205  shows LowerBound(B, s, functionImage(f, S, B), f(l))206proof207  have lA := LowerBound.member with bound208  have bounded := LowerBound.subset with bound209  refine ⟨(IsMonotoneMap.apply_member with h, lA), (functionImage.subset at f,210      S, B), ?_⟩211  intros v hv212  obtain ⟨vB, x, hx, rfl⟩ := functionImage.membership.forward with hv213  have below := LowerBound.below with bound, hx214  exact IsMonotoneMap.preserves with h, lA, (bounded with x, hx), below215216theorem IsMonotoneMap.image_supremum_le (f A r B s S u v : Set)217  requires h : IsMonotoneMap(f, A, r, B, s)218  requires hu : Supremum(A, r, S, u)219  requires hv : Supremum(B, s, functionImage(f, S, B), v)220  shows relates(s, v, f(u))221proof222  have uA := Supremum.member with hu223  have bound := IsMonotoneMap.image_upper with h, (Supremum.upper with hu)224  exact Supremum.least with hv, (IsMonotoneMap.apply_member with h, uA), bound225226theorem IsMonotoneMap.image_infimum_ge (f A r B s S l m : Set)227  requires h : IsMonotoneMap(f, A, r, B, s)228  requires hl : Infimum(A, r, S, l)229  requires hm : Infimum(B, s, functionImage(f, S, B), m)230  shows relates(s, f(l), m)231proof232  have lA := Infimum.member with hl233  have bound := IsMonotoneMap.image_lower with h, (Infimum.lower with hl)234  exact Infimum.greatest with hm, (IsMonotoneMap.apply_member with h, lA), bound235236theorem IsMonotoneMap.join_le (f A r B s x y : Set)237  requires h : IsMonotoneMap(f, A, r, B, s)238  requires source : IsLattice(A, r)239  requires target : IsLattice(B, s)240  requires hx : x ∈ A241  requires hy : y ∈ A242  shows relates(s, join(B, s, f(x), f(y)), f(join(A, r, x, y)))243proof244  have joinA := join.member with source, hx, hy245  have fxB := IsMonotoneMap.apply_member with h, hx246  have fyB := IsMonotoneMap.apply_member with h, hy247  have fJ := IsMonotoneMap.apply_member with h, joinA248  have xJ := IsMonotoneMap.preserves with h, hx, joinA,249      (join.upper_left with source, hx, hy)250  have yJ := IsMonotoneMap.preserves with h, hy, joinA,251      (join.upper_right with source, hx, hy)252  exact join.least with target, fxB, fyB, fJ, xJ, yJ253254theorem IsMonotoneMap.meet_ge (f A r B s x y : Set)255  requires h : IsMonotoneMap(f, A, r, B, s)256  requires source : IsLattice(A, r)257  requires target : IsLattice(B, s)258  requires hx : x ∈ A259  requires hy : y ∈ A260  shows relates(s, f(meet(A, r, x, y)), meet(B, s, f(x), f(y)))261proof262  have meetA := meet.member with source, hx, hy263  have fxB := IsMonotoneMap.apply_member with h, hx264  have fyB := IsMonotoneMap.apply_member with h, hy265  have fM := IsMonotoneMap.apply_member with h, meetA266  have mX := IsMonotoneMap.preserves with h, meetA, hx,267      (meet.lower_left with source, hx, hy)268  have mY := IsMonotoneMap.preserves with h, meetA, hy,269      (meet.lower_right with source, hx, hy)270  exact meet.greatest with target, fxB, fyB, fM, mX, mY271272-- Galois connections273274theorem IsGaloisConnection.lower_function (f A r g B s : Set)275  requires h : IsGaloisConnection(f, A, r, g, B, s)276  shows f : A → B277proof278  simp [IsGaloisConnection]279280theorem IsGaloisConnection.upper_function (f A r g B s : Set)281  requires h : IsGaloisConnection(f, A, r, g, B, s)282  shows g : B → A283proof284  simp [IsGaloisConnection]285286theorem IsGaloisConnection.adjunction (f A r g B s x y : Set)287  requires h : IsGaloisConnection(f, A, r, g, B, s)288  requires hx : x ∈ A289  requires hy : y ∈ B290  shows relates(s, f(x), y) ↔ relates(r, x, g(y))291proof292  rcases h with ⟨fFunction, gFunction, adjoint⟩293  exact adjoint with x, hx, y, hy294295theorem IsGaloisConnection.unit (f A r g B s x : Set)296  requires h : IsGaloisConnection(f, A, r, g, B, s)297  requires target : IsPartialOrder(B, s)298  requires hx : x ∈ A299  shows relates(r, x, g(f(x)))300proof301  have reflexive := IsPartialOrder.reflexive with target302  have fxB := FunctionBetween.apply_closed with303      (IsGaloisConnection.lower_function with h), hx304  have adjoint := IsGaloisConnection.adjunction with h, hx, fxB305  exact adjoint.forward with (reflexive with f(x), fxB)306307theorem IsGaloisConnection.counit (f A r g B s y : Set)308  requires h : IsGaloisConnection(f, A, r, g, B, s)309  requires source : IsPartialOrder(A, r)310  requires hy : y ∈ B311  shows relates(s, f(g(y)), y)312proof313  have reflexive := IsPartialOrder.reflexive with source314  have gyA := FunctionBetween.apply_closed with315      (IsGaloisConnection.upper_function with h), hy316  have adjoint := IsGaloisConnection.adjunction with h, gyA, hy317  exact adjoint.backward with (reflexive with g(y), gyA)318319theorem IsGaloisConnection.lower_monotone (f A r g B s : Set)320  requires h : IsGaloisConnection(f, A, r, g, B, s)321  requires source : IsPartialOrder(A, r)322  requires target : IsPartialOrder(B, s)323  shows IsMonotoneMap(f, A, r, B, s)324proof325  have transitive := IsPartialOrder.transitive with source326  have fFunction := IsGaloisConnection.lower_function with h327  have gFunction := IsGaloisConnection.upper_function with h328  constructor329  . exact fFunction330  . intros x hx y hy hxy331    have fyB := FunctionBetween.apply_closed with fFunction, hy332    have gfyA := FunctionBetween.apply_closed with gFunction, fyB333    have unit := IsGaloisConnection.unit with h, target, hy334    have below := transitive with x, hx, y, hy, g(f(y)), gfyA, hxy, unit335    have adjoint := IsGaloisConnection.adjunction with h, hx, fyB336    exact adjoint.backward with below337338theorem IsGaloisConnection.upper_monotone (f A r g B s : Set)339  requires h : IsGaloisConnection(f, A, r, g, B, s)340  requires source : IsPartialOrder(A, r)341  requires target : IsPartialOrder(B, s)342  shows IsMonotoneMap(g, B, s, A, r)343proof344  have transitive := IsPartialOrder.transitive with target345  have fFunction := IsGaloisConnection.lower_function with h346  have gFunction := IsGaloisConnection.upper_function with h347  constructor348  . exact gFunction349  . intros x hx y hy hxy350    have gxA := FunctionBetween.apply_closed with gFunction, hx351    have fgxB := FunctionBetween.apply_closed with fFunction, gxA352    have counit := IsGaloisConnection.counit with h, source, hx353    have below := transitive with f(g(x)), fgxB, x, hx, y, hy, counit, hxy354    have adjoint := IsGaloisConnection.adjunction with h, gxA, hy355    exact adjoint.forward with below356357theorem IsGaloisConnection.lower_upper_lower (f A r g B s x : Set)358  requires h : IsGaloisConnection(f, A, r, g, B, s)359  requires source : IsPartialOrder(A, r)360  requires target : IsPartialOrder(B, s)361  requires hx : x ∈ A362  shows f(g(f(x))) = f(x)363proof364  have antisymmetric := IsPartialOrder.antisymmetric with target365  have fFunction := IsGaloisConnection.lower_function with h366  have gFunction := IsGaloisConnection.upper_function with h367  have fxB := FunctionBetween.apply_closed with fFunction, hx368  have gfxA := FunctionBetween.apply_closed with gFunction, fxB369  have fgfxB := FunctionBetween.apply_closed with fFunction, gfxA370  have below := IsGaloisConnection.counit with h, source, fxB371  have unit := IsGaloisConnection.unit with h, target, hx372  have monotone := IsGaloisConnection.lower_monotone with h, source, target373  have above := IsMonotoneMap.preserves with monotone, hx, gfxA, unit374  exact antisymmetric with f(g(f(x))), fgfxB, f(x), fxB, below, above375376theorem IsGaloisConnection.upper_lower_upper (f A r g B s y : Set)377  requires h : IsGaloisConnection(f, A, r, g, B, s)378  requires source : IsPartialOrder(A, r)379  requires target : IsPartialOrder(B, s)380  requires hy : y ∈ B381  shows g(f(g(y))) = g(y)382proof383  have antisymmetric := IsPartialOrder.antisymmetric with source384  have fFunction := IsGaloisConnection.lower_function with h385  have gFunction := IsGaloisConnection.upper_function with h386  have gyA := FunctionBetween.apply_closed with gFunction, hy387  have fgyB := FunctionBetween.apply_closed with fFunction, gyA388  have gfgyA := FunctionBetween.apply_closed with gFunction, fgyB389  have above := IsGaloisConnection.unit with h, target, gyA390  have counit := IsGaloisConnection.counit with h, source, hy391  have monotone := IsGaloisConnection.upper_monotone with h, source, target392  have below := IsMonotoneMap.preserves with monotone, fgyB, hy, counit393  exact antisymmetric with g(f(g(y))), gfgyA, g(y), gyA, below, above394395theorem IsGaloisConnection.identity (A r : Set)396  shows IsGaloisConnection(identity(A), A, r, identity(A), A, r)397proof398  refine ⟨identity.function at A, identity.function at A, ?_⟩399  intros x hx y hy400  have valueX := identity.apply with hx401  have valueY := identity.apply with hy402  rw [valueX, valueY]403  constructor404  . intro related405    exact related406  . intro related407    exact related408409theorem IsGaloisConnection.compose (f A r g B s k C t l : Set)410  requires first : IsGaloisConnection(f, A, r, g, B, s)411  requires second : IsGaloisConnection(k, B, s, l, C, t)412  shows413    IsGaloisConnection(compose(k, f, A, B, C), A, r, compose(g, l, C, B, A), C, t)414proof415  have fFunction := IsGaloisConnection.lower_function with first416  have gFunction := IsGaloisConnection.upper_function with first417  have kFunction := IsGaloisConnection.lower_function with second418  have lFunction := IsGaloisConnection.upper_function with second419  refine ⟨(compose.function with fFunction, kFunction),420      (compose.function with lFunction, gFunction), ?_⟩421  intros x hx z hz422  have valueX := compose.apply with fFunction, kFunction, hx423  have valueZ := compose.apply with lFunction, gFunction, hz424  rw [valueX, valueZ]425  have fxB := FunctionBetween.apply_closed with fFunction, hx426  have lzB := FunctionBetween.apply_closed with lFunction, hz427  have outer := IsGaloisConnection.adjunction with second, fxB, hz428  have inner := IsGaloisConnection.adjunction with first, hx, lzB429  constructor430  . intro related431    exact inner.forward with (outer.forward with related)432  . intro related433    exact outer.backward with (inner.backward with related)434435-- The left adjoint preserves suprema and the right adjoint preserves infima.436437theorem IsGaloisConnection.lower_supremum (f A r g B s S u : Set)438  requires h : IsGaloisConnection(f, A, r, g, B, s)439  requires source : IsPartialOrder(A, r)440  requires target : IsPartialOrder(B, s)441  requires hu : Supremum(A, r, S, u)442  shows Supremum(B, s, functionImage(f, S, B), f(u))443proof444  have monotone := IsGaloisConnection.lower_monotone with h, source, target445  have gFunction := IsGaloisConnection.upper_function with h446  have uA := Supremum.member with hu447  have bounded := Supremum.subset with hu448  constructor449  . exact IsMonotoneMap.image_upper with monotone, (Supremum.upper with hu)450  . intros b hb bound451    have gbA := FunctionBetween.apply_closed with gFunction, hb452    have lifted : UpperBound(A, r, S, g(b))453      refine ⟨gbA, bounded, ?_⟩454      intros x hx455      have xA := bounded with x, hx456      have fxB := IsMonotoneMap.apply_member with monotone, xA457      have imageMember : f(x) ∈ functionImage(f, S, B) :=458        functionImage.membership.backward with ⟨fxB, x, hx, rfl⟩459      have above := UpperBound.above with bound, imageMember460      have adjoint := IsGaloisConnection.adjunction with h, xA, hb461      exact adjoint.forward with above462    have below := Supremum.least with hu, gbA, lifted463    have adjoint := IsGaloisConnection.adjunction with h, uA, hb464    exact adjoint.backward with below465466theorem IsGaloisConnection.upper_infimum (f A r g B s T v : Set)467  requires h : IsGaloisConnection(f, A, r, g, B, s)468  requires source : IsPartialOrder(A, r)469  requires target : IsPartialOrder(B, s)470  requires hv : Infimum(B, s, T, v)471  shows Infimum(A, r, functionImage(g, T, A), g(v))472proof473  have monotone := IsGaloisConnection.upper_monotone with h, source, target474  have fFunction := IsGaloisConnection.lower_function with h475  have vB := Infimum.member with hv476  have bounded := Infimum.subset with hv477  constructor478  . exact IsMonotoneMap.image_lower with monotone, (Infimum.lower with hv)479  . intros a ha bound480    have faB := FunctionBetween.apply_closed with fFunction, ha481    have lifted : LowerBound(B, s, T, f(a))482      refine ⟨faB, bounded, ?_⟩483      intros y hy484      have yB := bounded with y, hy485      have gyA := IsMonotoneMap.apply_member with monotone, yB486      have imageMember : g(y) ∈ functionImage(g, T, A) :=487        functionImage.membership.backward with ⟨gyA, y, hy, rfl⟩488      have below := LowerBound.below with bound, imageMember489      have adjoint := IsGaloisConnection.adjunction with h, ha, yB490      exact adjoint.backward with below491    have above := Infimum.greatest with hv, faB, lifted492    have adjoint := IsGaloisConnection.adjunction with h, ha, vB493    exact adjoint.forward with above494495-- Closure operators496497theorem IsClosureOperator.function (c A r : Set)498  requires h : IsClosureOperator(c, A, r)499  shows c : A → A500proof501  simp [IsClosureOperator]502503theorem IsClosureOperator.extensive (c A r x : Set)504  requires h : IsClosureOperator(c, A, r)505  requires hx : x ∈ A506  shows relates(r, x, c(x))507proof508  rcases h with ⟨function, extensive, monotone, idempotent⟩509  exact extensive with x, hx510511theorem IsClosureOperator.monotone (c A r : Set)512  requires h : IsClosureOperator(c, A, r)513  shows IsMonotoneMap(c, A, r, A, r)514proof515  rcases h with ⟨function, extensive, monotone, idempotent⟩516  refine ⟨function, monotone⟩517518theorem IsClosureOperator.idempotent (c A r x : Set)519  requires h : IsClosureOperator(c, A, r)520  requires hx : x ∈ A521  shows c(c(x)) = c(x)522proof523  rcases h with ⟨function, extensive, monotone, idempotent⟩524  exact idempotent with x, hx525526theorem IsClosureOperator.apply_member (c A r x : Set)527  requires h : IsClosureOperator(c, A, r)528  requires hx : x ∈ A529  shows c(x) ∈ A530proof531  exact FunctionBetween.apply_closed with (IsClosureOperator.function with h),532    hx533534theorem IsClosureOperator.identity (A r : Set)535  requires order : IsPartialOrder(A, r)536  shows IsClosureOperator(identity(A), A, r)537proof538  have reflexive := IsPartialOrder.reflexive with order539  refine ⟨identity.function at A, ?_, ?_, ?_⟩540  . intros x hx541    have valueX := identity.apply with hx542    rw valueX543    exact reflexive with x, hx544  . intros x hx y hy hxy545    have valueX := identity.apply with hx546    have valueY := identity.apply with hy547    rw [valueX, valueY]548    exact hxy549  . intros x hx550    have valueX := identity.apply with hx551    rw valueX552    rw valueX553    rfl554555theorem IsClosureOperator.le_iff (c A r x y : Set)556  requires h : IsClosureOperator(c, A, r)557  requires order : IsPartialOrder(A, r)558  requires hx : x ∈ A559  requires hy : y ∈ A560  shows relates(r, x, c(y)) ↔ relates(r, c(x), c(y))561proof562  have transitive := IsPartialOrder.transitive with order563  have monotone := IsClosureOperator.monotone with h564  have cxA := IsClosureOperator.apply_member with h, hx565  have cyA := IsClosureOperator.apply_member with h, hy566  constructor567  . intro below568    have mapped := IsMonotoneMap.preserves with monotone, hx, cyA, below569    have twice := IsClosureOperator.idempotent with h, hy570    rw twice at mapped571    exact mapped572  . intro below573    have extensive := IsClosureOperator.extensive with h, hx574    exact transitive with x, hx, c(x), cxA, c(y), cyA, extensive, below575576theorem IsGaloisConnection.closure (f A r g B s : Set)577  requires h : IsGaloisConnection(f, A, r, g, B, s)578  requires source : IsPartialOrder(A, r)579  requires target : IsPartialOrder(B, s)580  shows IsClosureOperator(compose(g, f, A, B, A), A, r)581proof582  have fFunction := IsGaloisConnection.lower_function with h583  have gFunction := IsGaloisConnection.upper_function with h584  have lower := IsGaloisConnection.lower_monotone with h, source, target585  have upper := IsGaloisConnection.upper_monotone with h, source, target586  have composite := IsMonotoneMap.compose with lower, upper587  refine ⟨(compose.function with fFunction, gFunction), ?_, ?_, ?_⟩588  . intros x hx589    have valueX := compose.apply with fFunction, gFunction, hx590    rw valueX591    exact IsGaloisConnection.unit with h, target, hx592  . intros x hx y hy hxy593    exact IsMonotoneMap.preserves with composite, hx, hy, hxy594  . intros x hx595    have fxB := FunctionBetween.apply_closed with fFunction, hx596    have gfxA := FunctionBetween.apply_closed with gFunction, fxB597    have valueX := compose.apply with fFunction, gFunction, hx598    have valueTwice := compose.apply with fFunction, gFunction, gfxA599    rw valueX600    rw valueTwice601    exact IsGaloisConnection.upper_lower_upper with h, source, target, fxB602