case intro
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type ?u.10841
B : Set M
s g : Set (α → M)
hg : Definable A L g
φ : Formula (L[[↑A]]) α
⊢ Definable A L (setOf (Formula.Realize φ) ∩ g)
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type ?u.10841
B : Set M
s f g : Set (α → M)
hf : Definable A L f
hg : Definable A L g
⊢ Definable A L (f ∩ g)
rcases hf with ⟨φ, rfl⟩
case intro.intro
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type ?u.10841
B : Set M
s : Set (α → M)
φ θ : Formula (L[[↑A]]) α
⊢ Definable A L (setOf (Formula.Realize φ) ∩ setOf (Formula.Realize θ))
case intro
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type ?u.10841
B : Set M
s g : Set (α → M)
hg : Definable A L g
φ : Formula (L[[↑A]]) α
⊢ Definable A L (setOf (Formula.Realize φ) ∩ g)
rcases hg with ⟨θ, rfl⟩
case intro.intro
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type ?u.10841
B : Set M
s : Set (α → M)
φ θ : Formula (L[[↑A]]) α
⊢ setOf (Formula.Realize φ) ∩ setOf (Formula.Realize θ) = setOf (Formula.Realize (φ ⊓ θ))
case intro.intro
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type ?u.10841
B : Set M
s : Set (α → M)
φ θ : Formula (L[[↑A]]) α
⊢ Definable A L (setOf (Formula.Realize φ) ∩ setOf (Formula.Realize θ))
refine' ⟨φ ⊓ θ, _⟩
case intro.intro.h
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type ?u.10841
B : Set M
s : Set (α → M)
φ θ : Formula (L[[↑A]]) α
x✝ : α → M
⊢ x✝ ∈ setOf (Formula.Realize φ) ∩ setOf (Formula.Realize θ) ↔ x✝ ∈ setOf (Formula.Realize (φ ⊓ θ))
case intro.intro
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type ?u.10841
B : Set M
s : Set (α → M)
φ θ : Formula (L[[↑A]]) α
⊢ setOf (Formula.Realize φ) ∩ setOf (Formula.Realize θ) = setOf (Formula.Realize (φ ⊓ θ))
ext
no goals
case intro.intro.h
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type ?u.10841
B : Set M
s : Set (α → M)
φ θ : Formula (L[[↑A]]) α
x✝ : α → M
⊢ x✝ ∈ setOf (Formula.Realize φ) ∩ setOf (Formula.Realize θ) ↔ x✝ ∈ setOf (Formula.Realize (φ ⊓ θ))
simp