α : Type u_1
β : Type ?u.4779
ι : Type u_2
ι' : Type ?u.4785
inst✝¹ : Lattice α
inst✝ : OrderBot α
s✝ t : Finset ι
f✝ : ι → α
i✝ i : ι
f : ι → α
s : Finset ι
hs : s ⊆ {i}
j : ι
hji : j ∈ {i}
hj : ¬j ∈ s
⊢ Disjoint (f j) ⊥
α : Type u_1
β : Type ?u.4779
ι : Type u_2
ι' : Type ?u.4785
inst✝¹ : Lattice α
inst✝ : OrderBot α
s✝ t : Finset ι
f✝ : ι → α
i✝ i : ι
f : ι → α
s : Finset ι
hs : s ⊆ {i}
j : ι
hji : j ∈ {i}
hj : ¬j ∈ s
⊢ Disjoint (f j) (sup s f)
rw [eq_empty_of_ssubset_singleton ⟨hs, fun h => hj (h hji)⟩, sup_empty]
no goals
α : Type u_1
β : Type ?u.4779
ι : Type u_2
ι' : Type ?u.4785
inst✝¹ : Lattice α
inst✝ : OrderBot α
s✝ t : Finset ι
f✝ : ι → α
i✝ i : ι
f : ι → α
s : Finset ι
hs : s ⊆ {i}
j : ι
hji : j ∈ {i}
hj : ¬j ∈ s
⊢ Disjoint (f j) ⊥
exact disjoint_bot_right