no goals
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type ?u.14150
B : Set M
s✝ : Set (α → M)
ι : Type u_1
f : ι → Set (α → M)
hf : ∀ (i : ι), Definable A L (f i)
s : Finset ι
⊢ Definable A L (Finset.sup s f)
classical
  refine' Finset.induction definable_empty (fun i s _ h => _) s
  rw [Finset.sup_insert]
  exact (hf i).union h
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type ?u.14150
B : Set M
s✝¹ : Set (α → M)
ι : Type u_1
f : ι → Set (α → M)
hf : ∀ (i : ι), Definable A L (f i)
s✝ : Finset ι
i : ι
s : Finset ι
x✝ : ¬i ∈ s
h : Definable A L (Finset.sup s f)
⊢ Definable A L (Finset.sup (insert i s) f)
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type ?u.14150
B : Set M
s✝ : Set (α → M)
ι : Type u_1
f : ι → Set (α → M)
hf : ∀ (i : ι), Definable A L (f i)
s : Finset ι
⊢ Definable A L (Finset.sup s f)
refine' Finset.induction definable_empty (fun i s _ h => _) s
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type ?u.14150
B : Set M
s✝¹ : Set (α → M)
ι : Type u_1
f : ι → Set (α → M)
hf : ∀ (i : ι), Definable A L (f i)
s✝ : Finset ι
i : ι
s : Finset ι
x✝ : ¬i ∈ s
h : Definable A L (Finset.sup s f)
⊢ Definable A L (f i ⊔ Finset.sup s f)
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type ?u.14150
B : Set M
s✝¹ : Set (α → M)
ι : Type u_1
f : ι → Set (α → M)
hf : ∀ (i : ι), Definable A L (f i)
s✝ : Finset ι
i : ι
s : Finset ι
x✝ : ¬i ∈ s
h : Definable A L (Finset.sup s f)
⊢ Definable A L (Finset.sup (insert i s) f)
rw [Finset.sup_insert]
no goals
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type ?u.14150
B : Set M
s✝¹ : Set (α → M)
ι : Type u_1
f : ι → Set (α → M)
hf : ∀ (i : ι), Definable A L (f i)
s✝ : Finset ι
i : ι
s : Finset ι
x✝ : ¬i ∈ s
h : Definable A L (Finset.sup s f)
⊢ Definable A L (f i ⊔ Finset.sup s f)
exact (hf i).union h