English
If f and g are monotone functions from a directed index set into α, then the supremum of the pointwise infima f(i) ⊓ g(i) equals the infimum of the supremums: ⨆ i, f(i) ⊓ g(i) = (⨆ i, f(i)) ⊓ (⨆ i, g(i)).
Русский
Если f и g непеременные (монотонные) функции от направленного множества индексов в α, то верхний предел по i от (f(i) ∧ g(i)) равен (верхний предел f) ∧ (верхний предел g).
LaTeX
$$$\bigvee_{i} (f(i) \wedge g(i)) = \left(\bigvee_{i} f(i)\right) \wedge \left(\bigvee_{i} g(i)\right)$$$
Lean4
theorem iSup_inf_of_monotone {ι : Type*} [Preorder ι] [IsDirected ι (· ≤ ·)] {f g : ι → α} (hf : Monotone f)
(hg : Monotone g) : ⨆ i, f i ⊓ g i = (⨆ i, f i) ⊓ ⨆ i, g i :=
by
refine (le_iSup_inf_iSup f g).antisymm ?_
rw [iSup_inf_iSup]
refine iSup_mono' fun i => ?_
rcases directed_of (· ≤ ·) i.1 i.2 with ⟨j, h₁, h₂⟩
exact ⟨j, inf_le_inf (hf h₁) (hg h₂)⟩
