α : Type u_2
β : Type u_1
γ : Type ?u.61525
ι : Sort ?u.61528
inst✝¹ : ConditionallyCompleteLattice α
s t : Set α
a b : α
inst✝ : SemilatticeSup β
f g : β → α
hf : Monotone f
hg : Antitone g
h : f ≤ g
n : β
⊢ (⨆ (n : β), f n) ∈ Icc (f n) (g n)
α : Type u_2
β : Type u_1
γ : Type ?u.61525
ι : Sort ?u.61528
inst✝¹ : ConditionallyCompleteLattice α
s t : Set α
a b : α
inst✝ : SemilatticeSup β
f g : β → α
hf : Monotone f
hg : Antitone g
h : f ≤ g
⊢ (⨆ (n : β), f n) ∈ ⋂ (n : β), Icc (f n) (g n)
refine' mem_iInter.2 fun n => _
α : Type u_2
β : Type u_1
γ : Type ?u.61525
ι : Sort ?u.61528
inst✝¹ : ConditionallyCompleteLattice α
s t : Set α
a b : α
inst✝ : SemilatticeSup β
f g : β → α
hf : Monotone f
hg : Antitone g
h : f ≤ g
n : β
this : Nonempty β
⊢ (⨆ (n : β), f n) ∈ Icc (f n) (g n)
α : Type u_2
β : Type u_1
γ : Type ?u.61525
ι : Sort ?u.61528
inst✝¹ : ConditionallyCompleteLattice α
s t : Set α
a b : α
inst✝ : SemilatticeSup β
f g : β → α
hf : Monotone f
hg : Antitone g
h : f ≤ g
n : β
⊢ (⨆ (n : β), f n) ∈ Icc (f n) (g n)
haveI : Nonempty β := ⟨n⟩
α : Type u_2
β : Type u_1
γ : Type ?u.61525
ι : Sort ?u.61528
inst✝¹ : ConditionallyCompleteLattice α
s t : Set α
a b : α
inst✝ : SemilatticeSup β
f g : β → α
hf : Monotone f
hg : Antitone g
h : f ≤ g
n : β
this✝ : Nonempty β
this : ∀ (m : β), f m ≤ g n
⊢ (⨆ (n : β), f n) ∈ Icc (f n) (g n)
α : Type u_2
β : Type u_1
γ : Type ?u.61525
ι : Sort ?u.61528
inst✝¹ : ConditionallyCompleteLattice α
s t : Set α
a b : α
inst✝ : SemilatticeSup β
f g : β → α
hf : Monotone f
hg : Antitone g
h : f ≤ g
n : β
this : Nonempty β
⊢ (⨆ (n : β), f n) ∈ Icc (f n) (g n)
have : ∀ m, f m ≤ g n := fun m => hf.forall_le_of_antitone hg h m n
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.61525
ι : Sort ?u.61528
inst✝¹ : ConditionallyCompleteLattice α
s t : Set α
a b : α
inst✝ : SemilatticeSup β
f g : β → α
hf : Monotone f
hg : Antitone g
h : f ≤ g
n : β
this✝ : Nonempty β
this : ∀ (m : β), f m ≤ g n
⊢ (⨆ (n : β), f n) ∈ Icc (f n) (g n)
exact ⟨le_ciSup ⟨g <| n, forall_range_iff.2 this⟩ _, ciSup_le this⟩