Theorem: LO.System.consistent_compact (Logic/Logic/System.lean)

State before:
S : Type u_1
F : Type u_2
inst✝⁵ : LogicalConnective F
inst✝⁴ : System F S
inst✝³ : DeductiveExplosion S
inst✝² : Collection F S
inst✝¹ : Axiomatized S
inst✝ : Compact S
𝓢 : S
⊢ Consistent 𝓢 ↔ ∀ 𝓕 ⊆ 𝓢, Collection.Finite 𝓕 → Consistent 𝓕
Tactic:
simp [←not_inconsistent_iff_consistent, inconsistent_compact (𝓢 := 𝓢)]
State after:
no goals