no goals
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' : Theory L
ι : Type u_1
T : ι → Theory L
⊢ IsSatisfiable (⋃ (i : ι), T i) ↔ ∀ (s : Finset ι), IsSatisfiable (⋃ (i : ι) (_ : i ∈ s), T i)
classical
  refine'
    ⟨fun h s => h.mono (Set.iUnion_mono fun _ => Set.iUnion_subset_iff.2 fun _ => refl _),
      fun h => _⟩
  rw [isSatisfiable_iff_isFinitelySatisfiable]
  intro s hs
  rw [Set.iUnion_eq_iUnion_finset] at hs
  obtain ⟨t, ht⟩ := Directed.exists_mem_subset_of_finset_subset_biUnion (by
    exact Monotone.directed_le fun t1 t2 (h : ∀ ⦃x⦄, x ∈ t1 → x ∈ t2) =>
      Set.iUnion_mono fun _ => Set.iUnion_mono' fun h1 => ⟨h h1, refl _⟩) hs
  exact (h t).mono ht
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' : Theory L
ι : Type u_1
T : ι → Theory L
h : ∀ (s : Finset ι), IsSatisfiable (⋃ (i : ι) (_ : i ∈ s), T i)
⊢ IsSatisfiable (⋃ (i : ι), T i)
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' : Theory L
ι : Type u_1
T : ι → Theory L
⊢ IsSatisfiable (⋃ (i : ι), T i) ↔ ∀ (s : Finset ι), IsSatisfiable (⋃ (i : ι) (_ : i ∈ s), T i)
refine'
  ⟨fun h s => h.mono (Set.iUnion_mono fun _ => Set.iUnion_subset_iff.2 fun _ => refl _),
    fun h => _⟩
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' : Theory L
ι : Type u_1
T : ι → Theory L
h : ∀ (s : Finset ι), IsSatisfiable (⋃ (i : ι) (_ : i ∈ s), T i)
⊢ IsFinitelySatisfiable (⋃ (i : ι), T i)
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' : Theory L
ι : Type u_1
T : ι → Theory L
h : ∀ (s : Finset ι), IsSatisfiable (⋃ (i : ι) (_ : i ∈ s), T i)
⊢ IsSatisfiable (⋃ (i : ι), T i)
rw [isSatisfiable_iff_isFinitelySatisfiable]
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' : Theory L
ι : Type u_1
T : ι → Theory L
h : ∀ (s : Finset ι), IsSatisfiable (⋃ (i : ι) (_ : i ∈ s), T i)
s : Finset (Sentence L)
hs : ↑s ⊆ ⋃ (i : ι), T i
⊢ IsSatisfiable ↑s
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' : Theory L
ι : Type u_1
T : ι → Theory L
h : ∀ (s : Finset ι), IsSatisfiable (⋃ (i : ι) (_ : i ∈ s), T i)
⊢ IsFinitelySatisfiable (⋃ (i : ι), T i)
intro s hs
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' : Theory L
ι : Type u_1
T : ι → Theory L
h : ∀ (s : Finset ι), IsSatisfiable (⋃ (i : ι) (_ : i ∈ s), T i)
s : Finset (Sentence L)
hs : ↑s ⊆ ⋃ (t : Finset ι) (i : ι) (_ : i ∈ t), T i
⊢ IsSatisfiable ↑s
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' : Theory L
ι : Type u_1
T : ι → Theory L
h : ∀ (s : Finset ι), IsSatisfiable (⋃ (i : ι) (_ : i ∈ s), T i)
s : Finset (Sentence L)
hs : ↑s ⊆ ⋃ (i : ι), T i
⊢ IsSatisfiable ↑s
rw [Set.iUnion_eq_iUnion_finset] at hs
case intro
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' : Theory L
ι : Type u_1
T : ι → Theory L
h : ∀ (s : Finset ι), IsSatisfiable (⋃ (i : ι) (_ : i ∈ s), T i)
s : Finset (Sentence L)
hs : ↑s ⊆ ⋃ (t : Finset ι) (i : ι) (_ : i ∈ t), T i
t : Finset ι
ht : ↑s ⊆ ⋃ (i : ι) (_ : i ∈ t), T i
⊢ IsSatisfiable ↑s
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' : Theory L
ι : Type u_1
T : ι → Theory L
h : ∀ (s : Finset ι), IsSatisfiable (⋃ (i : ι) (_ : i ∈ s), T i)
s : Finset (Sentence L)
hs : ↑s ⊆ ⋃ (t : Finset ι) (i : ι) (_ : i ∈ t), T i
⊢ IsSatisfiable ↑s
obtain ⟨t, ht⟩ := Directed.exists_mem_subset_of_finset_subset_biUnion (by
  exact Monotone.directed_le fun t1 t2 (h : ∀ ⦃x⦄, x ∈ t1 → x ∈ t2) =>
    Set.iUnion_mono fun _ => Set.iUnion_mono' fun h1 => ⟨h h1, refl _⟩) hs
no goals
case intro
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' : Theory L
ι : Type u_1
T : ι → Theory L
h : ∀ (s : Finset ι), IsSatisfiable (⋃ (i : ι) (_ : i ∈ s), T i)
s : Finset (Sentence L)
hs : ↑s ⊆ ⋃ (t : Finset ι) (i : ι) (_ : i ∈ t), T i
t : Finset ι
ht : ↑s ⊆ ⋃ (i : ι) (_ : i ∈ t), T i
⊢ IsSatisfiable ↑s
exact (h t).mono ht
no goals
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' : Theory L
ι : Type u_1
T : ι → Theory L
h : ∀ (s : Finset ι), IsSatisfiable (⋃ (i : ι) (_ : i ∈ s), T i)
s : Finset (Sentence L)
hs : ↑s ⊆ ⋃ (t : Finset ι) (i : ι) (_ : i ∈ t), T i
⊢ Directed (fun x x_1 => x ⊆ x_1) fun i => ⋃ (i_1 : ι) (_ : i_1 ∈ i), T i_1
exact Monotone.directed_le fun t1 t2 (h : ∀ ⦃x⦄, x ∈ t1 → x ∈ t2) =>
  Set.iUnion_mono fun _ => Set.iUnion_mono' fun h1 => ⟨h h1, refl _⟩