English
Given OrderGenerates T, the gi construction produces a Galois insertion between Set(T) and α^op, linking kernel and hull as adjoint operations.
Русский
Пусть имеется порождающий порядок T; построение gi даёт Galois вставку между Set(T) и α^op, связывая kernel и hull как сопряженные операции.
LaTeX
$$$gi(hG):\\; GaloisInsertion(\\alpha := Set\\ T)\\; (\\alpha^{op}) \\; (OrderDual.toDual \\circ kernel) \\; (hull\\ T \\circ OrderDual.ofDual).$$$
Lean4
/-- Intermediate value theorem for two functions: if `f` and `g` are two functions continuous
on a preconnected set `s` and for some `a b ∈ s` we have `f a ≤ g a` and `g b ≤ f b`,
then for some `x ∈ s` we have `f x = g x`. -/
theorem intermediate_value₂ {s : Set X} (hs : IsPreconnected s) {a b : X} (ha : a ∈ s) (hb : b ∈ s) {f g : X → α}
(hf : ContinuousOn f s) (hg : ContinuousOn g s) (ha' : f a ≤ g a) (hb' : g b ≤ f b) : ∃ x ∈ s, f x = g x :=
let ⟨x, hx⟩ :=
@intermediate_value_univ₂ s α _ _ _ _ (Subtype.preconnectedSpace hs) ⟨a, ha⟩ ⟨b, hb⟩ _ _
(continuousOn_iff_continuous_restrict.1 hf) (continuousOn_iff_continuous_restrict.1 hg) ha' hb'
⟨x, x.2, hx⟩
