L : Language
L' : Language
M : Type w
N : Type ?u.419567
P : Type ?u.419570
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n : ℕ
T T' : Theory L
h : ∀ (φ : Sentence L), φ ∈ T → M ⊨ φ
h' : ∀ (φ : Sentence L), φ ∈ T' → M ⊨ φ
⊢ ∀ (φ : Sentence L), φ ∈ T ∨ φ ∈ T' → M ⊨ φ
L : Language
L' : Language
M : Type w
N : Type ?u.419567
P : Type ?u.419570
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n : ℕ
T T' : Theory L
h : M ⊨ T
h' : M ⊨ T'
⊢ M ⊨ T ∪ T'
simp only [model_iff, Set.mem_union] at *
no goals
L : Language
L' : Language
M : Type w
N : Type ?u.419567
P : Type ?u.419570
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n : ℕ
T T' : Theory L
h : ∀ (φ : Sentence L), φ ∈ T → M ⊨ φ
h' : ∀ (φ : Sentence L), φ ∈ T' → M ⊨ φ
⊢ ∀ (φ : Sentence L), φ ∈ T ∨ φ ∈ T' → M ⊨ φ
exact fun φ hφ => hφ.elim (h _) (h' _)