case intro
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type ?u.15860
B : Set M
s✝ s : Set (α → M)
φ : Formula (L[[↑A]]) α
hφ : s = setOf (Formula.Realize φ)
⊢ Definable A L (sᶜ)
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type ?u.15860
B : Set M
s✝ s : Set (α → M)
hf : Definable A L s
⊢ Definable A L (sᶜ)
rcases hf with ⟨φ, hφ⟩
case intro
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type ?u.15860
B : Set M
s✝ s : Set (α → M)
φ : Formula (L[[↑A]]) α
hφ : s = setOf (Formula.Realize φ)
⊢ sᶜ = setOf (Formula.Realize (Formula.not φ))
case intro
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type ?u.15860
B : Set M
s✝ s : Set (α → M)
φ : Formula (L[[↑A]]) α
hφ : s = setOf (Formula.Realize φ)
⊢ Definable A L (sᶜ)
refine' ⟨φ.not, _⟩
case intro.h
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type ?u.15860
B : Set M
s✝ s : Set (α → M)
φ : Formula (L[[↑A]]) α
hφ : s = setOf (Formula.Realize φ)
v : α → M
⊢ v ∈ sᶜ ↔ v ∈ setOf (Formula.Realize (Formula.not φ))
case intro
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type ?u.15860
B : Set M
s✝ s : Set (α → M)
φ : Formula (L[[↑A]]) α
hφ : s = setOf (Formula.Realize φ)
⊢ sᶜ = setOf (Formula.Realize (Formula.not φ))
ext v
no goals
case intro.h
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type ?u.15860
B : Set M
s✝ s : Set (α → M)
φ : Formula (L[[↑A]]) α
hφ : s = setOf (Formula.Realize φ)
v : α → M
⊢ v ∈ sᶜ ↔ v ∈ setOf (Formula.Realize (Formula.not φ))
rw [hφ, compl_setOf, mem_setOf, mem_setOf, Formula.realize_not]