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

State before:
M : Type u_1
F : Type u_2
inst✝² : LogicalConnective F
𝓢 : Semantics F M
inst✝¹ : Tarski M
inst✝ : DecidableEq F
t : Finset F
⊢ ¬Satisfiable M ↑t ↔ Valid M (⋁Finset.image (fun x => ~x) t)
Tactic:
simp [Satisfiable, realizeSet_iff, Valid, Finset.map_disj]
State after:
no goals