Theorems · Theorem · order theory
GaloisConnection.le_u_l_trans
∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {l : α → β} {u : β → α},
GaloisConnection l u → ∀ {x y z : α}, x ≤ u (l y) → y ≤ u (l z) → x ≤ u (l z)If (l, u) is a Galois connection, then the relation x ≤ u (l y) is a transitive relation.
If l is a closure operator (Submodule.span, Subgroup.closure, ...) and u is the coercion to
Set, this reads as "if U is in the closure of V and V is in the closure of W then U is
in the closure of W".
- Defined in
- Mathlib.Order.GaloisConnection.Defs
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 10 from the axioms · uses propext, Quot.sound
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
- LE.le.transproof · cited by 3,151
- GaloisConnectionstatement and proof · cited by 253
- GaloisConnection.monotone_uproof · cited by 53
- GaloisConnection.l_leproof · cited by 28
Cited by2
Results whose statement or proof uses this declaration.
- Submodule.subset_span_transproof · cited by 1
- Projectivization.Subspace.subset_span_transproof · cited by 0