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

State before:
M : Type u_1
F : Type u_2
inst✝¹ : LogicalConnective F
𝓢 : Semantics F M
T : Set F
inst✝ : ∀ (𝓜 : M), Meaningful 𝓜
⊢ Satisfiable M T ↔ Meaningful (models M T)
Tactic:
simp [set_meaningful_iff_nonempty, satisfiableSet_iff_models_nonempty]
State after:
no goals