L : Language
T : Theory L
α : Type w
n : ℕ
h : IsMaximal T
φ : Sentence L
hφ : T ⊨ᵇ φ
con : Formula.not φ ∈ T
⊢ False
L : Language
T : Theory L
α : Type w
n : ℕ
h : IsMaximal T
φ : Sentence L
hφ : T ⊨ᵇ φ
⊢ φ ∈ T
refine' (h.mem_or_not_mem φ).resolve_right fun con => _
L : Language
T : Theory L
α : Type w
n : ℕ
h : IsMaximal T
φ : Sentence L
hφ : ¬IsSatisfiable T
con : Formula.not φ ∈ T
⊢ False
L : Language
T : Theory L
α : Type w
n : ℕ
h : IsMaximal T
φ : Sentence L
hφ : T ⊨ᵇ φ
con : Formula.not φ ∈ T
⊢ False
rw [models_iff_not_satisfiable, Set.union_singleton, Set.insert_eq_of_mem con] at hφ
no goals
L : Language
T : Theory L
α : Type w
n : ℕ
h : IsMaximal T
φ : Sentence L
hφ : ¬IsSatisfiable T
con : Formula.not φ ∈ T
⊢ False
exact hφ h.1