no goals
F : Type ?u.82158
α : Type u_2
β : Type u_1
γ : Type ?u.82167
ι : Type ?u.82170
κ : Type ?u.82173
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s s₁ s₂ : Finset β
f✝ g : β → α
a : α
f : β → α
S : Finset β
⊢ sup S f = ⊥ ↔ ∀ (s : β), s ∈ S → f s = ⊥
classical induction' S using Finset.induction with a S _ hi <;> simp [*]
no goals
F : Type ?u.82158
α : Type u_2
β : Type u_1
γ : Type ?u.82167
ι : Type ?u.82170
κ : Type ?u.82173
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s s₁ s₂ : Finset β
f✝ g : β → α
a : α
f : β → α
S : Finset β
⊢ sup S f = ⊥ ↔ ∀ (s : β), s ∈ S → f s = ⊥
induction' S using Finset.induction with a S _ hi <;> simp [*]