English
For every natural n, the map f ↦ f^[n] is monotone with respect to the pointwise order on CircleDeg1Lift.
Русский
Для каждого натурального n отображение f ↦ f^[n] монотонно по точечной частичной задаче CircleDeg1Lift.
LaTeX
$$$ \forall n \in \mathbb{N}, \; \text{Monotone}(f \mapsto f^{[n]}). $$$
Lean4
/-- Monotone circle maps form a lattice with respect to the pointwise order -/
noncomputable instance : Lattice CircleDeg1Lift
where
sup f
g :=
{ toFun := fun x => max (f x) (g x)
monotone' := fun _ _ h =>
max_le_max (f.mono h)
(g.mono h)
-- TODO: generalize to `Monotone.max`
map_add_one' := fun x => by simp [max_add_add_right] }
le f g := ∀ x, f x ≤ g x
le_refl f x := le_refl (f x)
le_trans _ _ _ h₁₂ h₂₃ x := le_trans (h₁₂ x) (h₂₃ x)
le_antisymm _ _ h₁₂ h₂₁ := ext fun x => le_antisymm (h₁₂ x) (h₂₁ x)
le_sup_left f g x := le_max_left (f x) (g x)
le_sup_right f g x := le_max_right (f x) (g x)
sup_le _ _ _ h₁ h₂ x := max_le (h₁ x) (h₂ x)
inf f
g :=
{ toFun := fun x => min (f x) (g x)
monotone' := fun _ _ h => min_le_min (f.mono h) (g.mono h)
map_add_one' := fun x => by simp [min_add_add_right] }
inf_le_left f g x := min_le_left (f x) (g x)
inf_le_right f g x := min_le_right (f x) (g x)
le_inf _ _ _ h₂ h₃ x := le_min (h₂ x) (h₃ x)
