Theorem: LO.FirstOrder.compact (Logic/FirstOrder/Ultraproduct.lean)

State before:
L : Language
T : Theory L
A : FinSubtheory T → Type u
s : (i : FinSubtheory T) → Structure L (A i)
⊢ Satisfiable T ↔ ∀ (u : Finset (Sentence L)), ↑u ⊆ T → Satisfiable ↑u
Tactic:
rw[compactness_aux]
State after:
L : Language
T : Theory L
A : FinSubtheory T → Type u
s : (i : FinSubtheory T) → Structure L (A i)
⊢ (∀ (i : FinSubtheory T), Satisfiable ↑↑i) ↔ ∀ (u : Finset (Sentence L)), ↑u ⊆ T → Satisfiable ↑u

State before:
L : Language
T : Theory L
A : FinSubtheory T → Type u
s : (i : FinSubtheory T) → Structure L (A i)
⊢ (∀ (i : FinSubtheory T), Satisfiable ↑↑i) ↔ ∀ (u : Finset (Sentence L)), ↑u ⊆ T → Satisfiable ↑u
Tactic:
simp
State after:
no goals