L : Language
L' : Language
M : Type w
N : Type u_1
P : Type ?u.600632
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
α : Type u'
β : Type v'
n : ℕ
T : Theory L
inst✝ : N ⊨ completeTheory L M
φ : Sentence L
h : N ⊨ φ
⊢ M ⊨ φ
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type ?u.600632
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
α : Type u'
β : Type v'
n : ℕ
T : Theory L
inst✝ : N ⊨ completeTheory L M
φ : Sentence L
⊢ N ⊨ φ ↔ M ⊨ φ
refine' ⟨fun h => _, (L.completeTheory M).realize_sentence_of_mem⟩
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type ?u.600632
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
α : Type u'
β : Type v'
n : ℕ
T : Theory L
inst✝ : N ⊨ completeTheory L M
φ : Sentence L
h : ¬M ⊨ φ
⊢ ¬N ⊨ φ
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type ?u.600632
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
α : Type u'
β : Type v'
n : ℕ
T : Theory L
inst✝ : N ⊨ completeTheory L M
φ : Sentence L
h : N ⊨ φ
⊢ M ⊨ φ
contrapose! h
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type ?u.600632
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
α : Type u'
β : Type v'
n : ℕ
T : Theory L
inst✝ : N ⊨ completeTheory L M
φ : Sentence L
h : M ⊨ Formula.not φ
⊢ N ⊨ Formula.not φ
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type ?u.600632
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
α : Type u'
β : Type v'
n : ℕ
T : Theory L
inst✝ : N ⊨ completeTheory L M
φ : Sentence L
h : ¬M ⊨ φ
⊢ ¬N ⊨ φ
rw [← Sentence.realize_not] at *
no goals
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type ?u.600632
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
α : Type u'
β : Type v'
n : ℕ
T : Theory L
inst✝ : N ⊨ completeTheory L M
φ : Sentence L
h : M ⊨ Formula.not φ
⊢ N ⊨ Formula.not φ
exact (L.completeTheory M).realize_sentence_of_mem (mem_completeTheory.2 h)