Theorem: Finset.map_disj (Logic/Logic/LogicSymbol.lean)

State before:
α : Type u_2
inst✝³ : LogicalConnective α
inst✝² : DecidableEq α
F : Type u_1
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
s : Finset α
⊢ f (⋁s) ↔ ∃ a ∈ s, f a
Tactic:
simpa using List.map_disj f s.toList
State after:
no goals