α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLinearOrder β
f g : α →o β
hf : Continuous f
hg : Continuous g
c : Chain α
z : β
⊢ ↑(f ⊓ g) (ωSup c) ≤ z ↔ ωSup (Chain.map c (f ⊓ g)) ≤ z
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLinearOrder β
f g : α →o β
hf : Continuous f
hg : Continuous g
⊢ Continuous (f ⊓ g)
refine' fun c => eq_of_forall_ge_iff fun z => _
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLinearOrder β
f g : α →o β
hf : Continuous f
hg : Continuous g
c : Chain α
z : β
⊢ (∀ (x x_1 : ℕ), ↑f (↑c x_1) ≤ z ∨ ↑g (↑c x) ≤ z) ↔ ∀ (i : ℕ), ↑f (↑c i) ≤ z ∨ ↑g (↑c i) ≤ z
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLinearOrder β
f g : α →o β
hf : Continuous f
hg : Continuous g
c : Chain α
z : β
⊢ ↑(f ⊓ g) (ωSup c) ≤ z ↔ ωSup (Chain.map c (f ⊓ g)) ≤ z
simp only [inf_le_iff, hf c, hg c, ωSup_le_iff, ←forall_or_left, ←forall_or_right,
           Chain.map_coe, OrderHom.coe_inf, ge_iff_le, Pi.inf_apply, Function.comp]
no goals
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLinearOrder β
f g : α →o β
hf : Continuous f
hg : Continuous g
c : Chain α
z : β
⊢ (∀ (x x_1 : ℕ), ↑f (↑c x_1) ≤ z ∨ ↑g (↑c x) ≤ z) ↔ ∀ (i : ℕ), ↑f (↑c i) ≤ z ∨ ↑g (↑c i) ≤ z
exact ⟨λ h _ => h _ _, λ h i j => (h (max j i)).imp (le_trans $ f.mono $ c.mono $ le_max_left _ _)
  (le_trans $ g.mono $ c.mono $ le_max_right _ _)⟩