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

State before:
M : Type u_1
F : Type u_2
inst✝¹ : LogicalConnective F
𝓢 : Semantics F M
inst✝ : Tarski M
f : F
⊢ Valid M (~f) ↔ ¬Satisfiable M {f}
Tactic:
simp [Valid, Satisfiable]
State after:
no goals