Theorem: LO.Semantics.realize_finset_disj (Logic/Logic/Semantics.lean)

State before:
M : Type u_1
F : Type u_2
inst✝¹ : LogicalConnective F
𝓢 : Semantics F M
inst✝ : Tarski M
𝓜 : M
s : Finset F
⊢ 𝓜 ⊧ ⋁s ↔ ∃ p ∈ s, 𝓜 ⊧ p
Tactic:
simp [Finset.disj]
State after:
no goals