L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' : Theory L
ι : Type u_1
inst✝ : Nonempty ι
T : ι → Theory L
h : Directed (fun x x_1 => x ⊆ x_1) T
h' : ∀ (i : ι), IsSatisfiable (T i)
⊢ IsSatisfiable (⋃ (i : ι), T i)
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' : Theory L
ι : Type u_1
inst✝ : Nonempty ι
T : ι → Theory L
h : Directed (fun x x_1 => x ⊆ x_1) T
⊢ IsSatisfiable (⋃ (i : ι), T i) ↔ ∀ (i : ι), IsSatisfiable (T i)
refine' ⟨fun h' i => h'.mono (Set.subset_iUnion _ _), fun h' => _⟩
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' : Theory L
ι : Type u_1
inst✝ : Nonempty ι
T : ι → Theory L
h : Directed (fun x x_1 => x ⊆ x_1) T
h' : ∀ (i : ι), IsSatisfiable (T i)
⊢ ∀ (T0 : Finset (Sentence L)), (↑T0 ⊆ ⋃ (i : ι), T i) → IsSatisfiable ↑T0
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' : Theory L
ι : Type u_1
inst✝ : Nonempty ι
T : ι → Theory L
h : Directed (fun x x_1 => x ⊆ x_1) T
h' : ∀ (i : ι), IsSatisfiable (T i)
⊢ IsSatisfiable (⋃ (i : ι), T i)
rw [isSatisfiable_iff_isFinitelySatisfiable, IsFinitelySatisfiable]
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' : Theory L
ι : Type u_1
inst✝ : Nonempty ι
T : ι → Theory L
h : Directed (fun x x_1 => x ⊆ x_1) T
h' : ∀ (i : ι), IsSatisfiable (T i)
T0 : Finset (Sentence L)
hT0 : ↑T0 ⊆ ⋃ (i : ι), T i
⊢ IsSatisfiable ↑T0
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' : Theory L
ι : Type u_1
inst✝ : Nonempty ι
T : ι → Theory L
h : Directed (fun x x_1 => x ⊆ x_1) T
h' : ∀ (i : ι), IsSatisfiable (T i)
⊢ ∀ (T0 : Finset (Sentence L)), (↑T0 ⊆ ⋃ (i : ι), T i) → IsSatisfiable ↑T0
intro T0 hT0
case intro
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' : Theory L
ι : Type u_1
inst✝ : Nonempty ι
T : ι → Theory L
h : Directed (fun x x_1 => x ⊆ x_1) T
h' : ∀ (i : ι), IsSatisfiable (T i)
T0 : Finset (Sentence L)
hT0 : ↑T0 ⊆ ⋃ (i : ι), T i
i : ι
hi : ↑T0 ⊆ T i
⊢ IsSatisfiable ↑T0
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' : Theory L
ι : Type u_1
inst✝ : Nonempty ι
T : ι → Theory L
h : Directed (fun x x_1 => x ⊆ x_1) T
h' : ∀ (i : ι), IsSatisfiable (T i)
T0 : Finset (Sentence L)
hT0 : ↑T0 ⊆ ⋃ (i : ι), T i
⊢ IsSatisfiable ↑T0
obtain ⟨i, hi⟩ := h.exists_mem_subset_of_finset_subset_biUnion hT0
no goals
case intro
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' : Theory L
ι : Type u_1
inst✝ : Nonempty ι
T : ι → Theory L
h : Directed (fun x x_1 => x ⊆ x_1) T
h' : ∀ (i : ι), IsSatisfiable (T i)
T0 : Finset (Sentence L)
hT0 : ↑T0 ⊆ ⋃ (i : ι), T i
i : ι
hi : ↑T0 ⊆ T i
⊢ IsSatisfiable ↑T0
exact (h' i).mono hi