iSup_inf_of_antitone — Mathlib

English

If f and g are antitone and indexed by a directed set (with swap), then the same distributive equality holds: ⨆ i, f(i) ⊓ g(i) = (⨆ i, f(i)) ⊓ (⨆ i, g(i)).

Русский

Если f и g антитонны и индексирует направленное множество с перестановкой порядка, то равенство распространения сохраняется: ⨆ i, f(i) ⊓ g(i) = (⨆ i, f(i)) ⊓ (⨆ i, g(i)).

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_antitone {ι : Type*} [Preorder ι] [IsDirected ι (swap (· ≤ ·))] {f g : ι → α} (hf : Antitone f)
    (hg : Antitone g) : ⨆ i, f i ⊓ g i = (⨆ i, f i) ⊓ ⨆ i, g i :=
  @iSup_inf_of_monotone α _ ιᵒᵈ _ _ f g hf.dual_left hg.dual_left

Похожие утверждения