α : Type u_3
β : Type ?u.51964
ι✝ : Type ?u.51967
ι'✝ : Type ?u.51970
inst✝ : CompleteLattice α
s : Set α
hs : SetIndependent s
t✝ : ι✝ → α
ht✝ : Independent t✝
ι : Sort u_1
ι' : Sort u_2
t : ι → α
f : ι' → ι
ht : Independent t
hf : Injective f
i✝ i : ι'
⊢ (⨆ (_ : i ≠ i✝), (t ∘ f) i) ≤ ⨆ (_ : f i ≠ f i✝), t (f i)
α : Type u_3
β : Type ?u.51964
ι✝ : Type ?u.51967
ι'✝ : Type ?u.51970
inst✝ : CompleteLattice α
s : Set α
hs : SetIndependent s
t✝ : ι✝ → α
ht✝ : Independent t✝
ι : Sort u_1
ι' : Sort u_2
t : ι → α
f : ι' → ι
ht : Independent t
hf : Injective f
i : ι'
⊢ (⨆ (j : ι') (_ : j ≠ i), (t ∘ f) j) ≤ ⨆ (j : ι) (_ : j ≠ f i), t j
refine' (iSup_mono fun i => _).trans (iSup_comp_le _ f)
no goals
α : Type u_3
β : Type ?u.51964
ι✝ : Type ?u.51967
ι'✝ : Type ?u.51970
inst✝ : CompleteLattice α
s : Set α
hs : SetIndependent s
t✝ : ι✝ → α
ht✝ : Independent t✝
ι : Sort u_1
ι' : Sort u_2
t : ι → α
f : ι' → ι
ht : Independent t
hf : Injective f
i✝ i : ι'
⊢ (⨆ (_ : i ≠ i✝), (t ∘ f) i) ≤ ⨆ (_ : f i ≠ f i✝), t (f i)
exact iSup_const_mono hf.ne