Loogle!

Result

Found 260 declarations mentioning GaloisConnection. Of these, only the first 200 are shown.

• GaloisConnection 📋 Mathlib.Order.GaloisConnection.Defs
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] (l : α → β) (u : β → α) : Prop
• GaloisConnection.id 📋 Mathlib.Order.GaloisConnection.Defs
  {α : Type u} [pα : Preorder α] : GaloisConnection id id
• GaloisConnection.monotone_l 📋 Mathlib.Order.GaloisConnection.Defs
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {u : α → β} {l : β → α} (gc : GaloisConnection l u) : Monotone l
• GaloisConnection.monotone_u 📋 Mathlib.Order.GaloisConnection.Defs
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) : Monotone u
• GaloisCoinsertion.gc 📋 Mathlib.Order.GaloisConnection.Defs
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {l : α → β} {u : β → α} (self : GaloisCoinsertion l u) : GaloisConnection l u
• GaloisInsertion.gc 📋 Mathlib.Order.GaloisConnection.Defs
  {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {l : α → β} {u : β → α} (self : GaloisInsertion l u) : GaloisConnection l u
• GaloisConnection.l_u_le 📋 Mathlib.Order.GaloisConnection.Defs
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {u : α → β} {l : β → α} (gc : GaloisConnection l u) (a : α) : l (u a) ≤ a
• GaloisConnection.le_u_l 📋 Mathlib.Order.GaloisConnection.Defs
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) (a : α) : a ≤ u (l a)
• GaloisConnection.l_u_l_eq_l 📋 Mathlib.Order.GaloisConnection.Defs
  {α : Type u} {β : Type v} [PartialOrder α] [Preorder β] {u : α → β} {l : β → α} (gc : GaloisConnection l u) (b : β) : l (u (l b)) = l b
• GaloisConnection.monotone_l_comp_u 📋 Mathlib.Order.GaloisConnection.Defs
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) : Monotone (l ∘ u)
• GaloisConnection.monotone_u_comp_l 📋 Mathlib.Order.GaloisConnection.Defs
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {u : α → β} {l : β → α} (gc : GaloisConnection l u) : Monotone (u ∘ l)
• GaloisConnection.u_l_u_eq_u 📋 Mathlib.Order.GaloisConnection.Defs
  {α : Type u} {β : Type v} [PartialOrder α] [Preorder β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) (b : β) : u (l (u b)) = u b
• GaloisConnection.liftOrderBot 📋 Mathlib.Order.GaloisConnection.Defs
  {α : Type u_1} {β : Type u_2} [Preorder α] [OrderBot α] [PartialOrder β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) : OrderBot β
• GaloisConnection.liftOrderTop 📋 Mathlib.Order.GaloisConnection.Defs
  {α : Type u_1} {β : Type u_2} [Preorder α] [OrderTop α] [PartialOrder β] {u : α → β} {l : β → α} (gc : GaloisConnection l u) : OrderTop β
• GaloisConnection.l_u_l_eq_l' 📋 Mathlib.Order.GaloisConnection.Defs
  {α : Type u} {β : Type v} [PartialOrder α] [Preorder β] {u : α → β} {l : β → α} (gc : GaloisConnection l u) : l ∘ u ∘ l = l
• GaloisConnection.toGaloisCoinsertion 📋 Mathlib.Order.GaloisConnection.Defs
  {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {u : α → β} {l : β → α} (gc : GaloisConnection l u) (h : ∀ (b : β), u (l b) ≤ b) : GaloisCoinsertion l u
• GaloisConnection.toGaloisInsertion 📋 Mathlib.Order.GaloisConnection.Defs
  {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) (h : ∀ (b : β), b ≤ l (u b)) : GaloisInsertion l u
• GaloisConnection.u_l_u_eq_u' 📋 Mathlib.Order.GaloisConnection.Defs
  {α : Type u} {β : Type v} [PartialOrder α] [Preorder β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) : u ∘ l ∘ u = u
• GaloisConnection.exists_eq_l 📋 Mathlib.Order.GaloisConnection.Defs
  {α : Type u} {β : Type v} [PartialOrder α] [Preorder β] {u : α → β} {l : β → α} (gc : GaloisConnection l u) (a : α) : (∃ b, a = l b) ↔ a = l (u a)
• GaloisConnection.exists_eq_u 📋 Mathlib.Order.GaloisConnection.Defs
  {α : Type u} {β : Type v} [PartialOrder α] [Preorder β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) (a : α) : (∃ b, a = u b) ↔ a = u (l a)
• GaloisConnection.l_le 📋 Mathlib.Order.GaloisConnection.Defs
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) {a : α} {b : β} : a ≤ u b → l a ≤ b
• GaloisConnection.le_u 📋 Mathlib.Order.GaloisConnection.Defs
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {u : α → β} {l : β → α} (gc : GaloisConnection l u) {a : α} {b : β} : l b ≤ a → b ≤ u a
• GaloisConnection.le_iff_le 📋 Mathlib.Order.GaloisConnection.Defs
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) {a : α} {b : β} : l a ≤ b ↔ a ≤ u b
• GaloisConnection.l_eq 📋 Mathlib.Order.GaloisConnection.Defs
  {α : Type u} {β : Type v} [PartialOrder α] [Preorder β] {u : α → β} {l : β → α} (gc : GaloisConnection l u) {z : α} {y : β} : l y = z ↔ ∀ (x : α), z ≤ x ↔ y ≤ u x
• GaloisConnection.l_unique 📋 Mathlib.Order.GaloisConnection.Defs
  {α : Type u} {β : Type v} [PartialOrder α] [Preorder β] {u : α → β} {l : β → α} (gc : GaloisConnection l u) {u' : α → β} {l' : β → α} (gc' : GaloisConnection l' u') (hu : ∀ (a : α), u a = u' a) {b : β} : l b = l' b
• GaloisConnection.u_eq 📋 Mathlib.Order.GaloisConnection.Defs
  {α : Type u} {β : Type v} [PartialOrder α] [Preorder β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) {z : α} {y : β} : u y = z ↔ ∀ (x : α), x ≤ z ↔ l x ≤ y
• GaloisConnection.u_unique 📋 Mathlib.Order.GaloisConnection.Defs
  {α : Type u} {β : Type v} [PartialOrder α] [Preorder β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) {l' : α → β} {u' : β → α} (gc' : GaloisConnection l' u') (hl : ∀ (a : α), l a = l' a) {b : β} : u b = u' b
• GaloisConnection.l_u_le_trans 📋 Mathlib.Order.GaloisConnection.Defs
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {u : α → β} {l : β → α} (gc : GaloisConnection l u) {x y z : α} (hxy : l (u y) ≤ x) (hyz : l (u z) ≤ y) : l (u z) ≤ x
• GaloisConnection.le_u_l_trans 📋 Mathlib.Order.GaloisConnection.Defs
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) {x y z : α} (hxy : x ≤ u (l y)) (hyz : y ≤ u (l z)) : x ≤ u (l z)
• GaloisConnection.compose 📋 Mathlib.Order.GaloisConnection.Defs
  {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {l1 : α → β} {u1 : β → α} {l2 : β → γ} {u2 : γ → β} (gc1 : GaloisConnection l1 u1) (gc2 : GaloisConnection l2 u2) : GaloisConnection (l2 ∘ l1) (u1 ∘ u2)
• GaloisConnection.monotone_intro 📋 Mathlib.Order.GaloisConnection.Defs
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {l : α → β} {u : β → α} (hu : Monotone u) (hl : Monotone l) (h_u_l : ∀ (a : α), a ≤ u (l a)) (h_l_u : ∀ (a : β), l (u a) ≤ a) : GaloisConnection l u
• GaloisConnection.l_u_bot 📋 Mathlib.Order.GaloisConnection.Defs
  {α : Type u} {β : Type v} [PartialOrder α] [Preorder β] [OrderBot α] {u : α → β} {l : β → α} (gc : GaloisConnection l u) : l (u ⊥) = ⊥
• GaloisConnection.u_l_top 📋 Mathlib.Order.GaloisConnection.Defs
  {α : Type u} {β : Type v} [PartialOrder α] [Preorder β] [OrderTop α] {l : α → β} {u : β → α} (gc : GaloisConnection l u) : u (l ⊤) = ⊤
• GaloisConnection.l_bot 📋 Mathlib.Order.GaloisConnection.Defs
  {α : Type u} {β : Type v} [PartialOrder α] [Preorder β] [OrderBot α] [OrderBot β] {u : α → β} {l : β → α} (gc : GaloisConnection l u) : l ⊥ = ⊥
• GaloisConnection.lt_iff_lt 📋 Mathlib.Order.GaloisConnection.Defs
  {α : Type u} {β : Type v} [LinearOrder α] [LinearOrder β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) {a : α} {b : β} : b < l a ↔ u b < a
• GaloisConnection.u_top 📋 Mathlib.Order.GaloisConnection.Defs
  {α : Type u} {β : Type v} [PartialOrder α] [Preorder β] [OrderTop α] [OrderTop β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) : u ⊤ = ⊤
• GaloisConnection.l_eq_bot 📋 Mathlib.Order.GaloisConnection.Defs
  {α : Type u} {β : Type v} [PartialOrder α] [Preorder β] [OrderBot α] {u : α → β} {l : β → α} (gc : GaloisConnection l u) {x : β} : l x = ⊥ ↔ x ≤ u ⊥
• GaloisConnection.u_eq_top 📋 Mathlib.Order.GaloisConnection.Defs
  {α : Type u} {β : Type v} [PartialOrder α] [Preorder β] [OrderTop α] {l : α → β} {u : β → α} (gc : GaloisConnection l u) {x : β} : u x = ⊤ ↔ l ⊤ ≤ x
• GaloisCoinsertion.mk 📋 Mathlib.Order.GaloisConnection.Defs
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {l : α → β} {u : β → α} (choice : (x : β) → x ≤ l (u x) → α) (gc : GaloisConnection l u) (u_l_le : ∀ (x : α), u (l x) ≤ x) (choice_eq : ∀ (a : β) (h : a ≤ l (u a)), choice a h = u a) : GaloisCoinsertion l u
• GaloisInsertion.mk 📋 Mathlib.Order.GaloisConnection.Defs
  {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {l : α → β} {u : β → α} (choice : (x : α) → u (l x) ≤ x → β) (gc : GaloisConnection l u) (le_l_u : ∀ (x : β), x ≤ l (u x)) (choice_eq : ∀ (a : α) (h : u (l a) ≤ a), choice a h = l a) : GaloisInsertion l u
• GaloisConnection.dfun 📋 Mathlib.Order.GaloisConnection.Defs
  {ι : Type u} {α : ι → Type v} {β : ι → Type w} [(i : ι) → Preorder (α i)] [(i : ι) → Preorder (β i)] (l : (i : ι) → α i → β i) (u : (i : ι) → β i → α i) (gc : ∀ (i : ι), GaloisConnection (l i) (u i)) : GaloisConnection (fun a i => l i (a i)) fun b i => u i (b i)
• GaloisConnection.l_comm_of_u_comm 📋 Mathlib.Order.GaloisConnection.Defs
  {X : Type u_1} [Preorder X] {Y : Type u_2} [Preorder Y] {Z : Type u_3} [Preorder Z] {W : Type u_4} [PartialOrder W] {lYX : X → Y} {uXY : Y → X} (hXY : GaloisConnection lYX uXY) {lWZ : Z → W} {uZW : W → Z} (hZW : GaloisConnection lWZ uZW) {lWY : Y → W} {uYW : W → Y} (hWY : GaloisConnection lWY uYW) {lZX : X → Z} {uXZ : Z → X} (hXZ : GaloisConnection lZX uXZ) (h : ∀ (w : W), uXZ (uZW w) = uXY (uYW w)) {x : X} : lWZ (lZX x) = lWY (lYX x)
• GaloisConnection.u_comm_of_l_comm 📋 Mathlib.Order.GaloisConnection.Defs
  {X : Type u_1} [PartialOrder X] {Y : Type u_2} [Preorder Y] {Z : Type u_3} [Preorder Z] {W : Type u_4} [Preorder W] {lYX : X → Y} {uXY : Y → X} (hXY : GaloisConnection lYX uXY) {lWZ : Z → W} {uZW : W → Z} (hZW : GaloisConnection lWZ uZW) {lWY : Y → W} {uYW : W → Y} (hWY : GaloisConnection lWY uYW) {lZX : X → Z} {uXZ : Z → X} (hXZ : GaloisConnection lZX uXZ) (h : ∀ (x : X), lWZ (lZX x) = lWY (lYX x)) {w : W} : uXZ (uZW w) = uXY (uYW w)
• GaloisConnection.l_comm_iff_u_comm 📋 Mathlib.Order.GaloisConnection.Defs
  {X : Type u_1} [PartialOrder X] {Y : Type u_2} [Preorder Y] {Z : Type u_3} [Preorder Z] {W : Type u_4} [PartialOrder W] {lYX : X → Y} {uXY : Y → X} (hXY : GaloisConnection lYX uXY) {lWZ : Z → W} {uZW : W → Z} (hZW : GaloisConnection lWZ uZW) {lWY : Y → W} {uYW : W → Y} (hWY : GaloisConnection lWY uYW) {lZX : X → Z} {uXZ : Z → X} (hXZ : GaloisConnection lZX uXZ) : (∀ (w : W), uXZ (uZW w) = uXY (uYW w)) ↔ ∀ (x : X), lWZ (lZX x) = lWY (lYX x)
• GaloisConnection.dual 📋 Mathlib.Order.GaloisConnection.Defs
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) : GaloisConnection (⇑OrderDual.toDual ∘ u ∘ ⇑OrderDual.ofDual) (⇑OrderDual.toDual ∘ l ∘ ⇑OrderDual.ofDual)
• gc_inf_himp 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_2} [GeneralizedHeytingAlgebra α] {a : α} : GaloisConnection (fun x => a ⊓ x) fun x => a ⇨ x
• gc_sdiff_sup 📋 Mathlib.Order.Heyting.Basic
  {α : Type u_2} [GeneralizedCoheytingAlgebra α] {a : α} : GaloisConnection (fun x => x \ a) fun x => a ⊔ x
• FloorSemiring.gc_ceil 📋 Mathlib.Algebra.Order.Floor.Defs
  {α : Type u_3} {inst✝ : Semiring α} {inst✝¹ : PartialOrder α} [self : FloorSemiring α] : GaloisConnection FloorSemiring.ceil Nat.cast
• Nat.gc_ceil_coe 📋 Mathlib.Algebra.Order.Floor.Defs
  {α : Type u_1} [Semiring α] [PartialOrder α] [FloorSemiring α] : GaloisConnection Nat.ceil Nat.cast
• FloorRing.gc_ceil_coe 📋 Mathlib.Algebra.Order.Floor.Defs
  {α : Type u_3} {inst✝ : Ring α} {inst✝¹ : LinearOrder α} [self : FloorRing α] : GaloisConnection FloorRing.ceil Int.cast
• FloorRing.gc_coe_floor 📋 Mathlib.Algebra.Order.Floor.Defs
  {α : Type u_3} {inst✝ : Ring α} {inst✝¹ : LinearOrder α} [self : FloorRing α] : GaloisConnection Int.cast FloorRing.floor
• Int.gc_ceil_coe 📋 Mathlib.Algebra.Order.Floor.Defs
  {α : Type u_1} [Ring α] [LinearOrder α] [FloorRing α] : GaloisConnection Int.ceil Int.cast
• Int.gc_coe_floor 📋 Mathlib.Algebra.Order.Floor.Defs
  {α : Type u_1} [Ring α] [LinearOrder α] [FloorRing α] : GaloisConnection Int.cast Int.floor
• FloorRing.ofCeil 📋 Mathlib.Algebra.Order.Floor.Defs
  (α : Type u_3) [Ring α] [LinearOrder α] [IsOrderedRing α] (ceil : α → ℤ) (gc_ceil_coe : GaloisConnection ceil Int.cast) : FloorRing α
• FloorRing.ofFloor 📋 Mathlib.Algebra.Order.Floor.Defs
  (α : Type u_3) [Ring α] [LinearOrder α] [IsOrderedRing α] (floor : α → ℤ) (gc_coe_floor : GaloisConnection Int.cast floor) : FloorRing α
• FloorRing.mk 📋 Mathlib.Algebra.Order.Floor.Defs
  {α : Type u_3} [Ring α] [LinearOrder α] (floor ceil : α → ℤ) (gc_coe_floor : GaloisConnection Int.cast floor) (gc_ceil_coe : GaloisConnection ceil Int.cast) : FloorRing α
• FloorSemiring.mk 📋 Mathlib.Algebra.Order.Floor.Defs
  {α : Type u_3} [Semiring α] [PartialOrder α] (floor ceil : α → ℕ) (floor_of_neg : ∀ {a : α}, a < 0 → floor a = 0) (gc_floor : ∀ {a : α} {n : ℕ}, 0 ≤ a → (n ≤ floor a ↔ ↑n ≤ a)) (gc_ceil : GaloisConnection ceil Nat.cast) : FloorSemiring α
• Nat.galoisConnection_mul_div 📋 Mathlib.Order.GaloisConnection.Basic
  {k : ℕ} (h : 0 < k) : GaloisConnection (fun n => n * k) fun n => n / k
• GaloisConnection.bddAbove_l_image 📋 Mathlib.Order.GaloisConnection.Basic
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) {s : Set α} : BddAbove (l '' s) ↔ BddAbove s
• GaloisConnection.bddBelow_u_image 📋 Mathlib.Order.GaloisConnection.Basic
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {u : α → β} {l : β → α} (gc : GaloisConnection l u) {s : Set α} : BddBelow (u '' s) ↔ BddBelow s
• GaloisConnection.isGLB_l 📋 Mathlib.Order.GaloisConnection.Basic
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) {a : α} : IsGLB {b | a ≤ u b} (l a)
• GaloisConnection.isGreatest_u 📋 Mathlib.Order.GaloisConnection.Basic
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {u : α → β} {l : β → α} (gc : GaloisConnection l u) {a : α} : IsGreatest {b | l b ≤ a} (u a)
• GaloisConnection.isLUB_u 📋 Mathlib.Order.GaloisConnection.Basic
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {u : α → β} {l : β → α} (gc : GaloisConnection l u) {a : α} : IsLUB {b | l b ≤ a} (u a)
• GaloisConnection.isLeast_l 📋 Mathlib.Order.GaloisConnection.Basic
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) {a : α} : IsLeast {b | a ≤ u b} (l a)
• GaloisConnection.isGLB_u_image 📋 Mathlib.Order.GaloisConnection.Basic
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {u : α → β} {l : β → α} (gc : GaloisConnection l u) {s : Set α} {a : α} (h : IsGLB s a) : IsGLB (u '' s) (u a)
• GaloisConnection.isLUB_l_image 📋 Mathlib.Order.GaloisConnection.Basic
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) {s : Set α} {a : α} (h : IsLUB s a) : IsLUB (l '' s) (l a)
• GaloisConnection.lowerBounds_u_image 📋 Mathlib.Order.GaloisConnection.Basic
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {u : α → β} {l : β → α} (gc : GaloisConnection l u) (s : Set α) : lowerBounds (u '' s) = l ⁻¹' lowerBounds s
• GaloisConnection.upperBounds_l_image 📋 Mathlib.Order.GaloisConnection.Basic
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) (s : Set α) : upperBounds (l '' s) = u ⁻¹' upperBounds s
• GaloisConnection.l_sup 📋 Mathlib.Order.GaloisConnection.Basic
  {α : Type u} {β : Type v} {a₁ a₂ : α} [SemilatticeSup α] [SemilatticeSup β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) : l (a₁ ⊔ a₂) = l a₁ ⊔ l a₂
• GaloisConnection.u_inf 📋 Mathlib.Order.GaloisConnection.Basic
  {β : Type u} {α : Type v} {b₁ b₂ : β} [SemilatticeInf β] [SemilatticeInf α] {u : β → α} {l : α → β} (gc : GaloisConnection l u) : u (b₁ ⊓ b₂) = u b₁ ⊓ u b₂
• gc_sSup_Iic 📋 Mathlib.Order.GaloisConnection.Basic
  {α : Type u} [CompleteSemilatticeSup α] : GaloisConnection sSup Set.Iic
• GaloisConnection.l_sSup_eq_sSup_image 📋 Mathlib.Order.GaloisConnection.Basic
  {α : Type u} {β : Type v} [CompleteLattice α] [CompleteLattice β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) {s : Set α} : l (sSup s) = sSup (l '' s)
• GaloisConnection.u_sInf_eq_sInf_image 📋 Mathlib.Order.GaloisConnection.Basic
  {α : Type u} {β : Type v} [CompleteLattice α] [CompleteLattice β] {u : α → β} {l : β → α} (gc : GaloisConnection l u) {s : Set α} : u (sInf s) = sInf (u '' s)
• GaloisConnection.l_iSup 📋 Mathlib.Order.GaloisConnection.Basic
  {α : Type u} {β : Type v} {ι : Sort x} [CompleteLattice α] [CompleteLattice β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) {f : ι → α} : l (iSup f) = ⨆ i, l (f i)
• GaloisConnection.u_iInf 📋 Mathlib.Order.GaloisConnection.Basic
  {α : Type u} {β : Type v} {ι : Sort x} [CompleteLattice α] [CompleteLattice β] {u : α → β} {l : β → α} (gc : GaloisConnection l u) {f : ι → α} : u (iInf f) = ⨅ i, u (f i)
• OrderIso.to_galoisConnection 📋 Mathlib.Order.GaloisConnection.Basic
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] (e : α ≃o β) : GaloisConnection ⇑e ⇑e.symm
• GaloisConnection.l_sSup 📋 Mathlib.Order.GaloisConnection.Basic
  {α : Type u} {β : Type v} [CompleteLattice α] [CompleteLattice β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) {s : Set α} : l (sSup s) = ⨆ a ∈ s, l a
• GaloisConnection.u_sInf 📋 Mathlib.Order.GaloisConnection.Basic
  {α : Type u} {β : Type v} [CompleteLattice α] [CompleteLattice β] {u : α → β} {l : β → α} (gc : GaloisConnection l u) {s : Set α} : u (sInf s) = ⨅ a ∈ s, u a
• isGLB_image2_of_isGLB_isGLB 📋 Mathlib.Order.GaloisConnection.Basic
  {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {s : Set α} {t : Set β} {u : α → β → γ} {u₁ : β → γ → α} {u₂ : α → γ → β} {a₀ : α} {b₀ : β} (h₁ : ∀ (b : β), GaloisConnection (u₁ b) (Function.swap u b)) (h₂ : ∀ (a : α), GaloisConnection (u₂ a) (u a)) (ha₀ : IsGLB s a₀) (hb₀ : IsGLB t b₀) : IsGLB (Set.image2 u s t) (u a₀ b₀)
• isLUB_image2_of_isLUB_isLUB 📋 Mathlib.Order.GaloisConnection.Basic
  {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {s : Set α} {t : Set β} {l : α → β → γ} {u₁ : β → γ → α} {u₂ : α → γ → β} {a₀ : α} {b₀ : β} (h₁ : ∀ (b : β), GaloisConnection (Function.swap l b) (u₁ b)) (h₂ : ∀ (a : α), GaloisConnection (l a) (u₂ a)) (ha₀ : IsLUB s a₀) (hb₀ : IsLUB t b₀) : IsLUB (Set.image2 l s t) (l a₀ b₀)
• GaloisConnection.l_iSup₂ 📋 Mathlib.Order.GaloisConnection.Basic
  {α : Type u} {β : Type v} {ι : Sort x} {κ : ι → Sort u_1} [CompleteLattice α] [CompleteLattice β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) {f : (i : ι) → κ i → α} : l (⨆ i, ⨆ j, f i j) = ⨆ i, ⨆ j, l (f i j)
• GaloisConnection.u_iInf₂ 📋 Mathlib.Order.GaloisConnection.Basic
  {α : Type u} {β : Type v} {ι : Sort x} {κ : ι → Sort u_1} [CompleteLattice α] [CompleteLattice β] {u : α → β} {l : β → α} (gc : GaloisConnection l u) {f : (i : ι) → κ i → α} : u (⨅ i, ⨅ j, f i j) = ⨅ i, ⨅ j, u (f i j)
• sInf_image2_eq_sInf_sInf 📋 Mathlib.Order.GaloisConnection.Basic
  {α : Type u} {β : Type v} {γ : Type w} [CompleteLattice α] [CompleteLattice β] [CompleteLattice γ] {s : Set α} {t : Set β} {u : α → β → γ} {u₁ : β → γ → α} {u₂ : α → γ → β} (h₁ : ∀ (b : β), GaloisConnection (u₁ b) (Function.swap u b)) (h₂ : ∀ (a : α), GaloisConnection (u₂ a) (u a)) : sInf (Set.image2 u s t) = u (sInf s) (sInf t)
• sSup_image2_eq_sSup_sSup 📋 Mathlib.Order.GaloisConnection.Basic
  {α : Type u} {β : Type v} {γ : Type w} [CompleteLattice α] [CompleteLattice β] [CompleteLattice γ] {s : Set α} {t : Set β} {l : α → β → γ} {u₁ : β → γ → α} {u₂ : α → γ → β} (h₁ : ∀ (b : β), GaloisConnection (Function.swap l b) (u₁ b)) (h₂ : ∀ (a : α), GaloisConnection (l a) (u₂ a)) : sSup (Set.image2 l s t) = l (sSup s) (sSup t)
• GaloisConnection.compl 📋 Mathlib.Order.GaloisConnection.Basic
  {α : Type u} {β : Type v} [BooleanAlgebra α] [BooleanAlgebra β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) : GaloisConnection (compl ∘ u ∘ compl) (compl ∘ l ∘ compl)
• gc_Ici_sInf 📋 Mathlib.Order.GaloisConnection.Basic
  {α : Type u} [CompleteSemilatticeInf α] : GaloisConnection (⇑OrderDual.toDual ∘ Set.Ici) (sInf ∘ ⇑OrderDual.ofDual)
• isGLB_image2_of_isGLB_isLUB 📋 Mathlib.Order.GaloisConnection.Basic
  {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {s : Set α} {t : Set β} {u : α → β → γ} {u₁ : β → γ → α} {u₂ : α → γ → β} {a₀ : α} {b₀ : β} (h₁ : ∀ (b : β), GaloisConnection (u₁ b) (Function.swap u b)) (h₂ : ∀ (a : α), GaloisConnection (⇑OrderDual.toDual ∘ u₂ a) (u a ∘ ⇑OrderDual.ofDual)) (ha₀ : IsGLB s a₀) (hb₀ : IsLUB t b₀) : IsGLB (Set.image2 u s t) (u a₀ b₀)
• isGLB_image2_of_isLUB_isGLB 📋 Mathlib.Order.GaloisConnection.Basic
  {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {s : Set α} {t : Set β} {u : α → β → γ} {u₁ : β → γ → α} {u₂ : α → γ → β} {a₀ : α} {b₀ : β} (h₁ : ∀ (b : β), GaloisConnection (⇑OrderDual.toDual ∘ u₁ b) (Function.swap u b ∘ ⇑OrderDual.ofDual)) (h₂ : ∀ (a : α), GaloisConnection (u₂ a) (u a)) (ha₀ : IsLUB s a₀) (hb₀ : IsGLB t b₀) : IsGLB (Set.image2 u s t) (u a₀ b₀)
• isLUB_image2_of_isGLB_isLUB 📋 Mathlib.Order.GaloisConnection.Basic
  {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {s : Set α} {t : Set β} {l : α → β → γ} {u₁ : β → γ → α} {u₂ : α → γ → β} {a₀ : α} {b₀ : β} (h₁ : ∀ (b : β), GaloisConnection (Function.swap l b ∘ ⇑OrderDual.ofDual) (⇑OrderDual.toDual ∘ u₁ b)) (h₂ : ∀ (a : α), GaloisConnection (l a) (u₂ a)) (ha₀ : IsGLB s a₀) (hb₀ : IsLUB t b₀) : IsLUB (Set.image2 l s t) (l a₀ b₀)
• isLUB_image2_of_isLUB_isGLB 📋 Mathlib.Order.GaloisConnection.Basic
  {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {s : Set α} {t : Set β} {l : α → β → γ} {u₁ : β → γ → α} {u₂ : α → γ → β} {a₀ : α} {b₀ : β} (h₁ : ∀ (b : β), GaloisConnection (Function.swap l b) (u₁ b)) (h₂ : ∀ (a : α), GaloisConnection (l a ∘ ⇑OrderDual.ofDual) (⇑OrderDual.toDual ∘ u₂ a)) (ha₀ : IsLUB s a₀) (hb₀ : IsGLB t b₀) : IsLUB (Set.image2 l s t) (l a₀ b₀)
• sInf_image2_eq_sInf_sSup 📋 Mathlib.Order.GaloisConnection.Basic
  {α : Type u} {β : Type v} {γ : Type w} [CompleteLattice α] [CompleteLattice β] [CompleteLattice γ] {s : Set α} {t : Set β} {u : α → β → γ} {u₁ : β → γ → α} {u₂ : α → γ → β} (h₁ : ∀ (b : β), GaloisConnection (u₁ b) (Function.swap u b)) (h₂ : ∀ (a : α), GaloisConnection (⇑OrderDual.toDual ∘ u₂ a) (u a ∘ ⇑OrderDual.ofDual)) : sInf (Set.image2 u s t) = u (sInf s) (sSup t)
• sInf_image2_eq_sSup_sInf 📋 Mathlib.Order.GaloisConnection.Basic
  {α : Type u} {β : Type v} {γ : Type w} [CompleteLattice α] [CompleteLattice β] [CompleteLattice γ] {s : Set α} {t : Set β} {u : α → β → γ} {u₁ : β → γ → α} {u₂ : α → γ → β} (h₁ : ∀ (b : β), GaloisConnection (⇑OrderDual.toDual ∘ u₁ b) (Function.swap u b ∘ ⇑OrderDual.ofDual)) (h₂ : ∀ (a : α), GaloisConnection (u₂ a) (u a)) : sInf (Set.image2 u s t) = u (sSup s) (sInf t)
• sSup_image2_eq_sInf_sSup 📋 Mathlib.Order.GaloisConnection.Basic
  {α : Type u} {β : Type v} {γ : Type w} [CompleteLattice α] [CompleteLattice β] [CompleteLattice γ] {s : Set α} {t : Set β} {l : α → β → γ} {u₁ : β → γ → α} {u₂ : α → γ → β} (h₁ : ∀ (b : β), GaloisConnection (Function.swap l b ∘ ⇑OrderDual.ofDual) (⇑OrderDual.toDual ∘ u₁ b)) (h₂ : ∀ (a : α), GaloisConnection (l a) (u₂ a)) : sSup (Set.image2 l s t) = l (sInf s) (sSup t)
• sSup_image2_eq_sSup_sInf 📋 Mathlib.Order.GaloisConnection.Basic
  {α : Type u} {β : Type v} {γ : Type w} [CompleteLattice α] [CompleteLattice β] [CompleteLattice γ] {s : Set α} {t : Set β} {l : α → β → γ} {u₁ : β → γ → α} {u₂ : α → γ → β} (h₁ : ∀ (b : β), GaloisConnection (Function.swap l b) (u₁ b)) (h₂ : ∀ (a : α), GaloisConnection (l a ∘ ⇑OrderDual.ofDual) (⇑OrderDual.toDual ∘ u₂ a)) : sSup (Set.image2 l s t) = l (sSup s) (sInf t)
• isGLB_image2_of_isLUB_isLUB 📋 Mathlib.Order.GaloisConnection.Basic
  {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {s : Set α} {t : Set β} {u : α → β → γ} {u₁ : β → γ → α} {u₂ : α → γ → β} {a₀ : α} {b₀ : β} (h₁ : ∀ (b : β), GaloisConnection (⇑OrderDual.toDual ∘ u₁ b) (Function.swap u b ∘ ⇑OrderDual.ofDual)) (h₂ : ∀ (a : α), GaloisConnection (⇑OrderDual.toDual ∘ u₂ a) (u a ∘ ⇑OrderDual.ofDual)) (ha₀ : IsLUB s a₀) (hb₀ : IsLUB t b₀) : IsGLB (Set.image2 u s t) (u a₀ b₀)
• isLUB_image2_of_isGLB_isGLB 📋 Mathlib.Order.GaloisConnection.Basic
  {α : Type u} {β : Type v} {γ : Type w} [Preorder α] [Preorder β] [Preorder γ] {s : Set α} {t : Set β} {l : α → β → γ} {u₁ : β → γ → α} {u₂ : α → γ → β} {a₀ : α} {b₀ : β} (h₁ : ∀ (b : β), GaloisConnection (Function.swap l b ∘ ⇑OrderDual.ofDual) (⇑OrderDual.toDual ∘ u₁ b)) (h₂ : ∀ (a : α), GaloisConnection (l a ∘ ⇑OrderDual.ofDual) (⇑OrderDual.toDual ∘ u₂ a)) (ha₀ : IsGLB s a₀) (hb₀ : IsGLB t b₀) : IsLUB (Set.image2 l s t) (l a₀ b₀)
• sInf_image2_eq_sSup_sSup 📋 Mathlib.Order.GaloisConnection.Basic
  {α : Type u} {β : Type v} {γ : Type w} [CompleteLattice α] [CompleteLattice β] [CompleteLattice γ] {s : Set α} {t : Set β} {u : α → β → γ} {u₁ : β → γ → α} {u₂ : α → γ → β} (h₁ : ∀ (b : β), GaloisConnection (⇑OrderDual.toDual ∘ u₁ b) (Function.swap u b ∘ ⇑OrderDual.ofDual)) (h₂ : ∀ (a : α), GaloisConnection (⇑OrderDual.toDual ∘ u₂ a) (u a ∘ ⇑OrderDual.ofDual)) : sInf (Set.image2 u s t) = u (sSup s) (sSup t)
• sSup_image2_eq_sInf_sInf 📋 Mathlib.Order.GaloisConnection.Basic
  {α : Type u} {β : Type v} {γ : Type w} [CompleteLattice α] [CompleteLattice β] [CompleteLattice γ] {s : Set α} {t : Set β} {l : α → β → γ} {u₁ : β → γ → α} {u₂ : α → γ → β} (h₁ : ∀ (b : β), GaloisConnection (Function.swap l b ∘ ⇑OrderDual.ofDual) (⇑OrderDual.toDual ∘ u₁ b)) (h₂ : ∀ (a : α), GaloisConnection (l a ∘ ⇑OrderDual.ofDual) (⇑OrderDual.toDual ∘ u₂ a)) : sSup (Set.image2 l s t) = l (sInf s) (sInf t)
• csInf_image2_eq_csInf_csInf 📋 Mathlib.Order.ConditionallyCompleteLattice.Basic
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} [ConditionallyCompleteLattice α] [ConditionallyCompleteLattice β] [ConditionallyCompleteLattice γ] {s : Set α} {t : Set β} {u : α → β → γ} {l₁ : β → γ → α} {l₂ : α → γ → β} (h₁ : ∀ (b : β), GaloisConnection (l₁ b) (Function.swap u b)) (h₂ : ∀ (a : α), GaloisConnection (l₂ a) (u a)) (hs₀ : s.Nonempty) (hs₁ : BddBelow s) (ht₀ : t.Nonempty) (ht₁ : BddBelow t) : sInf (Set.image2 u s t) = u (sInf s) (sInf t)
• csSup_image2_eq_csSup_csSup 📋 Mathlib.Order.ConditionallyCompleteLattice.Basic
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} [ConditionallyCompleteLattice α] [ConditionallyCompleteLattice β] [ConditionallyCompleteLattice γ] {s : Set α} {t : Set β} {l : α → β → γ} {u₁ : β → γ → α} {u₂ : α → γ → β} (h₁ : ∀ (b : β), GaloisConnection (Function.swap l b) (u₁ b)) (h₂ : ∀ (a : α), GaloisConnection (l a) (u₂ a)) (hs₀ : s.Nonempty) (hs₁ : BddAbove s) (ht₀ : t.Nonempty) (ht₁ : BddAbove t) : sSup (Set.image2 l s t) = l (sSup s) (sSup t)
• csInf_image2_eq_csInf_csSup 📋 Mathlib.Order.ConditionallyCompleteLattice.Basic
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} [ConditionallyCompleteLattice α] [ConditionallyCompleteLattice β] [ConditionallyCompleteLattice γ] {s : Set α} {t : Set β} {u : α → β → γ} {l₁ : β → γ → α} {l₂ : α → γ → β} (h₁ : ∀ (b : β), GaloisConnection (l₁ b) (Function.swap u b)) (h₂ : ∀ (a : α), GaloisConnection (⇑OrderDual.toDual ∘ l₂ a) (u a ∘ ⇑OrderDual.ofDual)) : s.Nonempty → BddBelow s → t.Nonempty → BddAbove t → sInf (Set.image2 u s t) = u (sInf s) (sSup t)
• csInf_image2_eq_csSup_csInf 📋 Mathlib.Order.ConditionallyCompleteLattice.Basic
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} [ConditionallyCompleteLattice α] [ConditionallyCompleteLattice β] [ConditionallyCompleteLattice γ] {s : Set α} {t : Set β} {u : α → β → γ} {l₁ : β → γ → α} {l₂ : α → γ → β} (h₁ : ∀ (b : β), GaloisConnection (⇑OrderDual.toDual ∘ l₁ b) (Function.swap u b ∘ ⇑OrderDual.ofDual)) (h₂ : ∀ (a : α), GaloisConnection (l₂ a) (u a)) : s.Nonempty → BddAbove s → t.Nonempty → BddBelow t → sInf (Set.image2 u s t) = u (sSup s) (sInf t)
• csSup_image2_eq_csInf_csSup 📋 Mathlib.Order.ConditionallyCompleteLattice.Basic
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} [ConditionallyCompleteLattice α] [ConditionallyCompleteLattice β] [ConditionallyCompleteLattice γ] {s : Set α} {t : Set β} {l : α → β → γ} {u₁ : β → γ → α} {u₂ : α → γ → β} (h₁ : ∀ (b : β), GaloisConnection (Function.swap l b ∘ ⇑OrderDual.ofDual) (⇑OrderDual.toDual ∘ u₁ b)) (h₂ : ∀ (a : α), GaloisConnection (l a) (u₂ a)) : s.Nonempty → BddBelow s → t.Nonempty → BddAbove t → sSup (Set.image2 l s t) = l (sInf s) (sSup t)
• csSup_image2_eq_csSup_csInf 📋 Mathlib.Order.ConditionallyCompleteLattice.Basic
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} [ConditionallyCompleteLattice α] [ConditionallyCompleteLattice β] [ConditionallyCompleteLattice γ] {s : Set α} {t : Set β} {l : α → β → γ} {u₁ : β → γ → α} {u₂ : α → γ → β} (h₁ : ∀ (b : β), GaloisConnection (Function.swap l b) (u₁ b)) (h₂ : ∀ (a : α), GaloisConnection (l a ∘ ⇑OrderDual.ofDual) (⇑OrderDual.toDual ∘ u₂ a)) : s.Nonempty → BddAbove s → t.Nonempty → BddBelow t → sSup (Set.image2 l s t) = l (sSup s) (sInf t)
• csInf_image2_eq_csSup_csSup 📋 Mathlib.Order.ConditionallyCompleteLattice.Basic
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} [ConditionallyCompleteLattice α] [ConditionallyCompleteLattice β] [ConditionallyCompleteLattice γ] {s : Set α} {t : Set β} {u : α → β → γ} {l₁ : β → γ → α} {l₂ : α → γ → β} (h₁ : ∀ (b : β), GaloisConnection (⇑OrderDual.toDual ∘ l₁ b) (Function.swap u b ∘ ⇑OrderDual.ofDual)) (h₂ : ∀ (a : α), GaloisConnection (⇑OrderDual.toDual ∘ l₂ a) (u a ∘ ⇑OrderDual.ofDual)) : s.Nonempty → BddAbove s → t.Nonempty → BddAbove t → sInf (Set.image2 u s t) = u (sSup s) (sSup t)
• csSup_image2_eq_csInf_csInf 📋 Mathlib.Order.ConditionallyCompleteLattice.Basic
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} [ConditionallyCompleteLattice α] [ConditionallyCompleteLattice β] [ConditionallyCompleteLattice γ] {s : Set α} {t : Set β} {l : α → β → γ} {u₁ : β → γ → α} {u₂ : α → γ → β} (h₁ : ∀ (b : β), GaloisConnection (Function.swap l b ∘ ⇑OrderDual.ofDual) (⇑OrderDual.toDual ∘ u₁ b)) (h₂ : ∀ (a : α), GaloisConnection (l a ∘ ⇑OrderDual.ofDual) (⇑OrderDual.toDual ∘ u₂ a)) : s.Nonempty → BddBelow s → t.Nonempty → BddBelow t → sSup (Set.image2 l s t) = l (sInf s) (sInf t)
• Set.sUnion_powerset_gc 📋 Mathlib.Data.Set.Lattice.Bounded
  {α : Type u_1} : GaloisConnection (fun x => ⋃₀ x) fun x => 𝒫 x
• Set.image_preimage 📋 Mathlib.Data.Set.Lattice.Image
  {α : Type u_1} {β : Type u_2} {f : α → β} : GaloisConnection (Set.image f) (Set.preimage f)
• Set.preimage_kernImage 📋 Mathlib.Data.Set.Lattice.Image
  {α : Type u_1} {β : Type u_2} {f : α → β} : GaloisConnection (Set.preimage f) (Set.kernImage f)
• AddSubmonoid.gc_map_comap 📋 Mathlib.Algebra.Group.Submonoid.Operations
  {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [FunLike F M N] [mc : AddMonoidHomClass F M N] (f : F) : GaloisConnection (AddSubmonoid.map f) (AddSubmonoid.comap f)
• Submonoid.gc_map_comap 📋 Mathlib.Algebra.Group.Submonoid.Operations
  {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [FunLike F M N] [mc : MonoidHomClass F M N] (f : F) : GaloisConnection (Submonoid.map f) (Submonoid.comap f)
• AddSubgroup.gc_map_comap 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [AddGroup G] {N : Type u_4} [AddGroup N] (f : G →+ N) : GaloisConnection (AddSubgroup.map f) (AddSubgroup.comap f)
• Subgroup.gc_map_comap 📋 Mathlib.Algebra.Group.Subgroup.Map
  {G : Type u_1} [Group G] {N : Type u_4} [Group N] (f : G →* N) : GaloisConnection (Subgroup.map f) (Subgroup.comap f)
• Finset.gc_map_inl_toLeft 📋 Mathlib.Data.Finset.Sum
  {α : Type u_1} {β : Type u_2} : GaloisConnection (fun x => Finset.map Function.Embedding.inl x) Finset.toLeft
• Finset.gc_map_inr_toRight 📋 Mathlib.Data.Finset.Sum
  {α : Type u_1} {β : Type u_2} : GaloisConnection (fun x => Finset.map Function.Embedding.inr x) Finset.toRight
• GaloisConnection.l_csSup_of_directedOn' 📋 Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
  {α : Type u_1} {β : Type u_2} [ConditionallyCompletePartialOrderSup α] [ConditionallyCompletePartialOrderSup β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) {s : Set α} (hd : DirectedOn (fun x1 x2 => x1 ≤ x2) s) (hne : s.Nonempty) (hbdd : BddAbove s) : l (sSup s) = sSup (l '' s)
• GaloisConnection.u_csInf_of_directedOn' 📋 Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
  {α : Type u_1} {β : Type u_2} [ConditionallyCompletePartialOrderInf α] [ConditionallyCompletePartialOrderInf β] {l : α → β} {u : β → α} (gc : GaloisConnection u l) {s : Set α} (hd : DirectedOn (fun x1 x2 => x2 ≤ x1) s) (hne : s.Nonempty) (hbdd : BddBelow s) : l (sInf s) = sInf (l '' s)
• GaloisConnection.l_ciSup_of_directed 📋 Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
  {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [ConditionallyCompletePartialOrderSup α] [ConditionallyCompletePartialOrderSup β] [Nonempty ι] {l : α → β} {u : β → α} (gc : GaloisConnection l u) {f : ι → α} (hd : Directed (fun x1 x2 => x1 ≤ x2) f) (hf : BddAbove (Set.range f)) : l (⨆ i, f i) = ⨆ i, l (f i)
• GaloisConnection.u_ciInf_of_directed 📋 Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
  {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [ConditionallyCompletePartialOrderInf α] [ConditionallyCompletePartialOrderInf β] [Nonempty ι] {l : α → β} {u : β → α} (gc : GaloisConnection u l) {f : ι → α} (hd : Directed (fun x1 x2 => x2 ≤ x1) f) (hf : BddBelow (Set.range f)) : l (⨅ i, f i) = ⨅ i, l (f i)
• GaloisConnection.l_csSup_of_directedOn 📋 Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
  {α : Type u_1} {β : Type u_2} [ConditionallyCompletePartialOrderSup α] [ConditionallyCompletePartialOrderSup β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) {s : Set α} (hd : DirectedOn (fun x1 x2 => x1 ≤ x2) s) (hne : s.Nonempty) (hbdd : BddAbove s) : l (sSup s) = ⨆ x, l ↑x
• GaloisConnection.u_csInf_of_directedOn 📋 Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
  {α : Type u_1} {β : Type u_2} [ConditionallyCompletePartialOrderInf α] [ConditionallyCompletePartialOrderInf β] {l : α → β} {u : β → α} (gc : GaloisConnection u l) {s : Set α} (hd : DirectedOn (fun x1 x2 => x2 ≤ x1) s) (hne : s.Nonempty) (hbdd : BddBelow s) : l (sInf s) = ⨅ x, l ↑x
• GaloisConnection.l_ciSup_set_of_directedOn 📋 Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} [ConditionallyCompletePartialOrderSup α] [ConditionallyCompletePartialOrderSup β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) {s : Set γ} {f : γ → α} (hd : DirectedOn (fun x1 x2 => x1 ≤ x2) (f '' s)) (hf : BddAbove (f '' s)) (hne : s.Nonempty) : l (⨆ i, f ↑i) = ⨆ i, l (f ↑i)
• GaloisConnection.u_ciInf_set_of_directedOn 📋 Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} [ConditionallyCompletePartialOrderInf α] [ConditionallyCompletePartialOrderInf β] {l : α → β} {u : β → α} (gc : GaloisConnection u l) {s : Set γ} {f : γ → α} (hd : DirectedOn (fun x1 x2 => x2 ≤ x1) (f '' s)) (hf : BddBelow (f '' s)) (hne : s.Nonempty) : l (⨅ i, f ↑i) = ⨅ i, l (f ↑i)
• GaloisConnection.l_csSup' 📋 Mathlib.Order.ConditionallyCompleteLattice.Indexed
  {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLattice α] [ConditionallyCompleteLattice β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) {s : Set α} (hne : s.Nonempty) (hbdd : BddAbove s) : l (sSup s) = sSup (l '' s)
• GaloisConnection.u_csInf' 📋 Mathlib.Order.ConditionallyCompleteLattice.Indexed
  {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLattice α] [ConditionallyCompleteLattice β] {l : α → β} {u : β → α} (gc : GaloisConnection u l) {s : Set α} (hne : s.Nonempty) (hbdd : BddBelow s) : l (sInf s) = sInf (l '' s)
• GaloisConnection.l_ciSup 📋 Mathlib.Order.ConditionallyCompleteLattice.Indexed
  {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [ConditionallyCompleteLattice α] [ConditionallyCompleteLattice β] [Nonempty ι] {l : α → β} {u : β → α} (gc : GaloisConnection l u) {f : ι → α} (hf : BddAbove (Set.range f)) : l (⨆ i, f i) = ⨆ i, l (f i)
• GaloisConnection.u_ciInf 📋 Mathlib.Order.ConditionallyCompleteLattice.Indexed
  {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [ConditionallyCompleteLattice α] [ConditionallyCompleteLattice β] [Nonempty ι] {l : α → β} {u : β → α} (gc : GaloisConnection u l) {f : ι → α} (hf : BddBelow (Set.range f)) : l (⨅ i, f i) = ⨅ i, l (f i)
• GaloisConnection.l_csSup 📋 Mathlib.Order.ConditionallyCompleteLattice.Indexed
  {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLattice α] [ConditionallyCompleteLattice β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) {s : Set α} (hne : s.Nonempty) (hbdd : BddAbove s) : l (sSup s) = ⨆ x, l ↑x
• GaloisConnection.u_csInf 📋 Mathlib.Order.ConditionallyCompleteLattice.Indexed
  {α : Type u_1} {β : Type u_2} [ConditionallyCompleteLattice α] [ConditionallyCompleteLattice β] {l : α → β} {u : β → α} (gc : GaloisConnection u l) {s : Set α} (hne : s.Nonempty) (hbdd : BddBelow s) : l (sInf s) = ⨅ x, l ↑x
• GaloisConnection.l_ciSup_set 📋 Mathlib.Order.ConditionallyCompleteLattice.Indexed
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} [ConditionallyCompleteLattice α] [ConditionallyCompleteLattice β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) {s : Set γ} {f : γ → α} (hf : BddAbove (f '' s)) (hne : s.Nonempty) : l (⨆ i, f ↑i) = ⨆ i, l (f ↑i)
• GaloisConnection.u_ciInf_set 📋 Mathlib.Order.ConditionallyCompleteLattice.Indexed
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} [ConditionallyCompleteLattice α] [ConditionallyCompleteLattice β] {l : α → β} {u : β → α} (gc : GaloisConnection u l) {s : Set γ} {f : γ → α} (hf : BddBelow (f '' s)) (hne : s.Nonempty) : l (⨅ i, f ↑i) = ⨅ i, l (f ↑i)
• Order.gc_pred_succ 📋 Mathlib.Order.SuccPred.Basic
  {α : Type u_1} [Preorder α] [SuccOrder α] [PredOrder α] : GaloisConnection Order.pred Order.succ
• Cardinal.toENatAux_gc 📋 Mathlib.SetTheory.Cardinal.ENat
  : GaloisConnection Cardinal.ofENat Cardinal.toENatAux
• Cardinal.enat_gc 📋 Mathlib.SetTheory.Cardinal.ENat
  : GaloisConnection Cardinal.ofENat ⇑Cardinal.toENat
• Submodule.gc_map_comap 📋 Mathlib.Algebra.Module.Submodule.Map
  {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [RingHomSurjective σ₁₂] (f : M →ₛₗ[σ₁₂] M₂) : GaloisConnection (Submodule.map f) (Submodule.comap f)
• AddSubsemigroup.gc_map_comap 📋 Mathlib.Algebra.Group.Subsemigroup.Operations
  {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : M →ₙ+ N) : GaloisConnection (AddSubsemigroup.map f) (AddSubsemigroup.comap f)
• Subsemigroup.gc_map_comap 📋 Mathlib.Algebra.Group.Subsemigroup.Operations
  {M : Type u_1} {N : Type u_2} [Mul M] [Mul N] (f : M →ₙ* N) : GaloisConnection (Subsemigroup.map f) (Subsemigroup.comap f)
• NonUnitalSubsemiring.gc_map_comap 📋 Mathlib.RingTheory.NonUnitalSubsemiring.Basic
  {R : Type u} {S : Type v} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] {F : Type u_1} [FunLike F R S] [NonUnitalRingHomClass F R S] (f : F) : GaloisConnection (NonUnitalSubsemiring.map f) (NonUnitalSubsemiring.comap f)
• Subsemiring.gc_map_comap 📋 Mathlib.Algebra.Ring.Subsemiring.Basic
  {R : Type u} {S : Type v} [NonAssocSemiring R] [NonAssocSemiring S] (f : R →+* S) : GaloisConnection (Subsemiring.map f) (Subsemiring.comap f)
• NonUnitalSubring.gc_map_comap 📋 Mathlib.RingTheory.NonUnitalSubring.Basic
  {F : Type w} {R : Type u} {S : Type v} [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] [FunLike F R S] [NonUnitalRingHomClass F R S] (f : F) : GaloisConnection (NonUnitalSubring.map f) (NonUnitalSubring.comap f)
• Subring.gc_map_comap 📋 Mathlib.Algebra.Ring.Subring.Basic
  {R : Type u} {S : Type v} [NonAssocRing R] [NonAssocRing S] (f : R →+* S) : GaloisConnection (Subring.map f) (Subring.comap f)
• GaloisConnection.lowerAdjoint 📋 Mathlib.Order.Closure
  {α : Type u_1} {β : Type u_4} [Preorder α] [Preorder β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) : LowerAdjoint u
• LowerAdjoint.mk 📋 Mathlib.Order.Closure
  {α : Type u_1} {β : Type u_4} [Preorder α] [Preorder β] {u : β → α} (toFun : α → β) (gc' : GaloisConnection toFun u) : LowerAdjoint u
• GaloisConnection.closureOperator 📋 Mathlib.Order.Closure
  {α : Type u_1} {β : Type u_4} [PartialOrder α] [Preorder β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) : ClosureOperator α
• LowerAdjoint.gc 📋 Mathlib.Order.Closure
  {α : Type u_1} {β : Type u_4} [Preorder α] [Preorder β] {u : β → α} (l : LowerAdjoint u) : GaloisConnection l.toFun u
• LowerAdjoint.gc' 📋 Mathlib.Order.Closure
  {α : Type u_1} {β : Type u_4} [Preorder α] [Preorder β] {u : β → α} (self : LowerAdjoint u) : GaloisConnection self.toFun u
• GaloisConnection.lowerAdjoint_toFun 📋 Mathlib.Order.Closure
  {α : Type u_1} {β : Type u_4} [Preorder α] [Preorder β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) (a✝ : α) : gc.lowerAdjoint.toFun a✝ = l a✝
• GaloisConnection.closureOperator_isClosed 📋 Mathlib.Order.Closure
  {α : Type u_1} {β : Type u_4} [PartialOrder α] [Preorder β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) (x : α) : gc.closureOperator.IsClosed x = (u (l x) = x)
• GaloisConnection.closureOperator_apply 📋 Mathlib.Order.Closure
  {α : Type u_1} {β : Type u_4} [PartialOrder α] [Preorder β] {l : α → β} {u : β → α} (gc : GaloisConnection l u) (x : α) : gc.closureOperator x = u (l x)
• Filter.gc_comap_kernMap 📋 Mathlib.Order.Filter.Map
  {α : Type u_1} {β : Type u_2} (m : α → β) : GaloisConnection (Filter.comap m) (Filter.kernMap m)
• Filter.gc_map_comap 📋 Mathlib.Order.Filter.Map
  {α : Type u_1} {β : Type u_2} (m : α → β) : GaloisConnection (Filter.map m) (Filter.comap m)
• GaloisConnection.isCofinal_range 📋 Mathlib.Order.Cofinal
  {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : β → α} {g : α → β} (h : GaloisConnection f g) : IsCofinal (Set.range g)
• GaloisConnection.map_cofinal 📋 Mathlib.Order.Cofinal
  {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : β → α} {g : α → β} (h : GaloisConnection f g) {s : Set α} (hs : IsCofinal s) : IsCofinal (g '' s)
• GaloisConnection.map_isCofinal 📋 Mathlib.Order.Cofinal
  {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : β → α} {g : α → β} (h : GaloisConnection f g) {s : Set α} (hs : IsCofinal s) : IsCofinal (g '' s)
• GaloisConnection.cof_le 📋 Mathlib.SetTheory.Cardinal.Cofinality.Basic
  {α γ : Type u} [Preorder α] [Preorder γ] {f : γ → α} {g : α → γ} (h : GaloisConnection f g) : Order.cof γ ≤ Order.cof α
• GaloisConnection.cof_le_lift 📋 Mathlib.SetTheory.Cardinal.Cofinality.Basic
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : β → α} {g : α → β} (h : GaloisConnection f g) : Cardinal.lift.{u, v} (Order.cof β) ≤ Cardinal.lift.{v, u} (Order.cof α)
• Cardinal.gc_ord_card 📋 Mathlib.SetTheory.Ordinal.Basic
  : GaloisConnection Cardinal.ord Ordinal.card
• Ordinal.mul_div_gc 📋 Mathlib.SetTheory.Ordinal.Arithmetic
  {a : Ordinal.{u_4}} (ha : a ≠ 0) : GaloisConnection (fun x => a * x) fun x => x / a
• Submodule.dualAnnihilator_gc 📋 Mathlib.LinearAlgebra.Dual.Defs
  (R : Type u_1) (M : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] : GaloisConnection (⇑OrderDual.toDual ∘ Submodule.dualAnnihilator) (Submodule.dualCoannihilator ∘ ⇑OrderDual.ofDual)
• Sublattice.gc_map_comap 📋 Mathlib.Order.Sublattice
  {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] (f : LatticeHom α β) : GaloisConnection (Sublattice.map f) (Sublattice.comap f)
• SetRel.image_core_gc 📋 Mathlib.Basic.Rel
  {α : Type u_1} {β : Type u_2} {R : SetRel α β} : GaloisConnection R.image R.core
• Ideal.gc_map_comap 📋 Mathlib.RingTheory.Ideal.Maps
  {R : Type u} {S : Type v} {F : Type u_1} [Semiring R] [Semiring S] [FunLike F R S] (f : F) [RingHomClass F R S] : GaloisConnection (Ideal.map f) (Ideal.comap f)
• NonUnitalSubalgebra.gc_map_comap 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [NonUnitalNonAssocSemiring B] [Module R A] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] (f : F) : GaloisConnection (NonUnitalSubalgebra.map f) (NonUnitalSubalgebra.comap f)
• NonUnitalAlgebra.gc 📋 Mathlib.Algebra.Algebra.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] : GaloisConnection (NonUnitalAlgebra.adjoin R) SetLike.coe
• Subalgebra.gc_map_comap 📋 Mathlib.Algebra.Algebra.Subalgebra.Basic
  {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] (f : A →ₐ[R] B) : GaloisConnection (Subalgebra.map f) (Subalgebra.comap f)
• Algebra.gc 📋 Mathlib.Algebra.Algebra.Subalgebra.Lattice
  {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] : GaloisConnection (Algebra.adjoin R) SetLike.coe
• Subfield.gc_map_comap 📋 Mathlib.Algebra.Field.Subfield.Basic
  {K : Type u} {L : Type v} [DivisionRing K] [DivisionRing L] (f : K →+* L) : GaloisConnection (Subfield.map f) (Subfield.comap f)
• fixingAddSubgroup_fixedPoints_gc 📋 Mathlib.GroupTheory.GroupAction.FixingSubgroup
  (M : Type u_1) (α : Type u_2) [AddGroup M] [AddAction M α] : GaloisConnection (⇑OrderDual.toDual ∘ fixingAddSubgroup M) ((fun P => AddAction.fixedPoints (↥P) α) ∘ ⇑OrderDual.ofDual)
• fixingSubgroup_fixedPoints_gc 📋 Mathlib.GroupTheory.GroupAction.FixingSubgroup
  (M : Type u_1) (α : Type u_2) [Group M] [MulAction M α] : GaloisConnection (⇑OrderDual.toDual ∘ fixingSubgroup M) ((fun P => MulAction.fixedPoints (↥P) α) ∘ ⇑OrderDual.ofDual)
• fixingAddSubmonoid_fixedPoints_gc 📋 Mathlib.GroupTheory.GroupAction.FixingSubgroup
  (M : Type u_1) (α : Type u_2) [AddMonoid M] [AddAction M α] : GaloisConnection (⇑OrderDual.toDual ∘ fixingAddSubmonoid M) ((fun P => AddAction.fixedPoints (↥P) α) ∘ ⇑OrderDual.ofDual)
• fixingSubmonoid_fixedPoints_gc 📋 Mathlib.GroupTheory.GroupAction.FixingSubgroup
  (M : Type u_1) (α : Type u_2) [Monoid M] [MulAction M α] : GaloisConnection (⇑OrderDual.toDual ∘ fixingSubmonoid M) ((fun P => MulAction.fixedPoints (↥P) α) ∘ ⇑OrderDual.ofDual)
• NonUnitalStarSubalgebra.gc_map_comap 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Star A] [NonUnitalNonAssocSemiring B] [Module R B] [Star B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] [StarHomClass F A B] (f : F) : GaloisConnection (NonUnitalStarSubalgebra.map f) (NonUnitalStarSubalgebra.comap f)
• NonUnitalStarAlgebra.gc 📋 Mathlib.Algebra.Star.NonUnitalSubalgebra
  {R : Type u} {A : Type v} [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] : GaloisConnection (NonUnitalStarAlgebra.adjoin R) SetLike.coe
• StarAlgebra.gc 📋 Mathlib.Algebra.Star.Subalgebra
  {R : Type u_1} {A : Type u_2} [CommSemiring R] [StarRing R] [Semiring A] [Algebra R A] [StarRing A] [StarModule R A] : GaloisConnection (StarAlgebra.adjoin R) SetLike.coe
• StarSubalgebra.gc_map_comap 📋 Mathlib.Algebra.Star.Subalgebra
  {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [StarRing R] [Semiring A] [StarRing A] [Algebra R A] [StarModule R A] [Semiring B] [StarRing B] [Algebra R B] [StarModule R B] (f : A →⋆ₐ[R] B) : GaloisConnection (StarSubalgebra.map f) (StarSubalgebra.comap f)
• CategoryTheory.MorphismProperty.gc_strictMap 📋 Mathlib.CategoryTheory.MorphismProperty.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] (F : CategoryTheory.Functor C D) : GaloisConnection (fun x => x.strictMap F) fun x => x.inverseImage F
• TwoSidedIdeal.gc 📋 Mathlib.RingTheory.TwoSidedIdeal.Operations
  {R : Type u_1} [Ring R] : GaloisConnection ⇑TwoSidedIdeal.fromIdeal ⇑TwoSidedIdeal.asIdeal
• ofAddUnits_addUnits_gc 📋 Mathlib.Algebra.Group.Submonoid.Units
  {M : Type u_1} [AddMonoid M] : GaloisConnection AddSubgroup.ofAddUnits AddSubmonoid.addUnits
• ofUnits_units_gc 📋 Mathlib.Algebra.Group.Submonoid.Units
  {M : Type u_1} [Monoid M] : GaloisConnection Subgroup.ofUnits Submonoid.units
• gc_nhds 📋 Mathlib.Topology.Order
  {α : Type u} (a : α) : GaloisConnection (nhdsAdjoint a) fun t => nhds a
• gc_coinduced_induced 📋 Mathlib.Topology.Order
  {α : Type u_1} {β : Type u_2} (f : α → β) : GaloisConnection (TopologicalSpace.coinduced f) (TopologicalSpace.induced f)
• TopologicalSpace.gc_generateFrom 📋 Mathlib.Topology.Order
  (α : Type u_1) : GaloisConnection (fun t => OrderDual.toDual {s | IsOpen s}) (TopologicalSpace.generateFrom ∘ ⇑OrderDual.ofDual)
• Filter.bind_smallSets_gc 📋 Mathlib.Order.Filter.SmallSets
  {α : Type u_1} : GaloisConnection (fun L => L.bind Filter.principal) Filter.smallSets
• gc_lowerClosure_coe 📋 Mathlib.Order.UpperLower.Closure
  {α : Type u_1} [Preorder α] : GaloisConnection lowerClosure SetLike.coe
• gc_upperClosure_coe 📋 Mathlib.Order.UpperLower.Closure
  {α : Type u_1} [Preorder α] : GaloisConnection (⇑OrderDual.toDual ∘ upperClosure) (SetLike.coe ∘ ⇑OrderDual.ofDual)
• UniformFun.gc 📋 Mathlib.Topology.UniformSpace.UniformConvergenceTopology
  (α : Type u_1) (β : Type u_2) : GaloisConnection (fun 𝓐 => Filter.map (UniformFun.phi α β) (𝓐 ×ˢ ⊤)) fun 𝓕 => UniformFun.filter α β 𝓕
• GaloisConnection.leftOrdContinuous 📋 Mathlib.Order.OrdContinuous
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {g : β → α} (gc : GaloisConnection f g) : LeftOrdContinuous f
• GaloisConnection.rightOrdContinuous 📋 Mathlib.Order.OrdContinuous
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] {f : α → β} {g : β → α} (gc : GaloisConnection f g) : RightOrdContinuous g
• PrimeSpectrum.gc_set 📋 Mathlib.RingTheory.Spectrum.Prime.Basic
  (R : Type u) [CommSemiring R] : GaloisConnection (fun s => PrimeSpectrum.zeroLocus s) fun t => ↑(PrimeSpectrum.vanishingIdeal t)
• PrimeSpectrum.gc 📋 Mathlib.RingTheory.Spectrum.Prime.Basic
  (R : Type u) [CommSemiring R] : GaloisConnection (fun I => PrimeSpectrum.zeroLocus ↑I) fun t => PrimeSpectrum.vanishingIdeal t
• BooleanSubalgebra.gc_map_comap 📋 Mathlib.Order.BooleanSubalgebra
  {α : Type u_2} {β : Type u_3} [BooleanAlgebra α] [BooleanAlgebra β] (f : BoundedLatticeHom α β) : GaloisConnection (BooleanSubalgebra.map f) (BooleanSubalgebra.comap f)
• TopologicalSpace.Opens.gc 📋 Mathlib.Topology.Sets.Opens
  {α : Type u_2} [TopologicalSpace α] : GaloisConnection SetLike.coe TopologicalSpace.Opens.interior
• TopologicalSpace.Closeds.gc 📋 Mathlib.Topology.Sets.Closeds
  {α : Type u_2} [TopologicalSpace α] : GaloisConnection TopologicalSpace.Closeds.closure SetLike.coe
• Submodule.torsion_gc 📋 Mathlib.Algebra.Module.Torsion.Basic
  (R : Type u_1) (M : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] : GaloisConnection Submodule.annihilator fun I => Submodule.torsionBySet R M ↑(OrderDual.ofDual I)
• Submodule.orthogonalBilin_gc 📋 Mathlib.LinearAlgebra.SesquilinearForm.Orthogonal
  {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_4} {M₁ : Type u_5} {M₂ : Type u_6} [CommSemiring R] [CommSemiring R₁] [CommSemiring R₂] [AddCommMonoid M] [Module R M] [AddCommMonoid M₁] [Module R₁ M₁] [AddCommMonoid M₂] [Module R₂ M₂] {I₁ : R₁ →+* R} {I₂ : R₂ →+* R} (B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M) : GaloisConnection (Submodule.orthogonalBilin B) (Submodule.orthogonalBilin B.flip)
• CategoryTheory.Presieve.galoisConnection_pushforward_pullback 📋 Mathlib.CategoryTheory.Sites.Sieves.Presieve
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : Y ⟶ X) : GaloisConnection (CategoryTheory.Presieve.pushforward f) (CategoryTheory.Presieve.pullback f)
• CategoryTheory.Sieve.galoisConnection 📋 Mathlib.CategoryTheory.Sites.Sieves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : Y ⟶ X) : GaloisConnection (CategoryTheory.Sieve.pushforward f) (CategoryTheory.Sieve.pullback f)
• CategoryTheory.Presieve.galoisConnection_map_functorPullback 📋 Mathlib.CategoryTheory.Sites.Sieves.Functoriality
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (X : C) : GaloisConnection (CategoryTheory.Presieve.map F) (CategoryTheory.Presieve.functorPullback F)
• CategoryTheory.Sieve.functor_galoisConnection 📋 Mathlib.CategoryTheory.Sites.Sieves.Functoriality
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (X : C) : GaloisConnection (CategoryTheory.Sieve.functorPushforward F) (CategoryTheory.Sieve.functorPullback F)
• CategoryTheory.ObjectProperty.galoisConnection_isColocal 📋 Mathlib.CategoryTheory.Localization.Bousfield
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] : GaloisConnection (⇑OrderDual.toDual ∘ CategoryTheory.ObjectProperty.isColocal) (CategoryTheory.MorphismProperty.isColocal ∘ ⇑OrderDual.ofDual)

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using the Loogle command from the command palette. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. By subexpression:
   🔍 _ * (_ ^ _)
   finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

   The pattern can also be non-linear, as in
   🔍 Real.sqrt ?a * Real.sqrt ?a

   If the pattern has parameters, they are matched in any order. Both of these will find List.map:
   🔍 (?a -> ?b) -> List ?a -> List ?b
   🔍 List ?a -> (?a -> ?b) -> List ?b

4. By main conclusion:
   🔍 |- tsum _ = _ * tsum _
   finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

   As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
   🔍 |- _ < _ → tsum _ < tsum _
   will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

5. You can filter for definitions vs theorems: Using ⊢ (_ : Type _) finds all definitions which provide data while ⊢ (_ : Prop) finds all theorems (and definitions of proofs).

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO. Please review the Lean FRO Terms of Use and Privacy Policy.

This is Loogle revision 9f11169 serving mathlib revision 69fae59