case intro
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s : Set (α → M)
f : α → β
φ : Formula (L[[↑A]]) α
⊢ Definable A L ((fun g => g ∘ f) ⁻¹' setOf (Formula.Realize φ))
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
f : α → β
s : Set (α → M)
h : Definable A L s
⊢ Definable A L ((fun g => g ∘ f) ⁻¹' s)
obtain ⟨φ, rfl⟩ := h
case intro
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s : Set (α → M)
f : α → β
φ : Formula (L[[↑A]]) α
⊢ (fun g => g ∘ f) ⁻¹' setOf (Formula.Realize φ) = setOf (Formula.Realize (Formula.relabel f φ))
case intro
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s : Set (α → M)
f : α → β
φ : Formula (L[[↑A]]) α
⊢ Definable A L ((fun g => g ∘ f) ⁻¹' setOf (Formula.Realize φ))
refine' ⟨φ.relabel f, _⟩
case intro.h
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s : Set (α → M)
f : α → β
φ : Formula (L[[↑A]]) α
x✝ : β → M
⊢ x✝ ∈ (fun g => g ∘ f) ⁻¹' setOf (Formula.Realize φ) ↔ x✝ ∈ setOf (Formula.Realize (Formula.relabel f φ))
case intro
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s : Set (α → M)
f : α → β
φ : Formula (L[[↑A]]) α
⊢ (fun g => g ∘ f) ⁻¹' setOf (Formula.Realize φ) = setOf (Formula.Realize (Formula.relabel f φ))
ext
no goals
case intro.h
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s : Set (α → M)
f : α → β
φ : Formula (L[[↑A]]) α
x✝ : β → M
⊢ x✝ ∈ (fun g => g ∘ f) ⁻¹' setOf (Formula.Realize φ) ↔ x✝ ∈ setOf (Formula.Realize (Formula.relabel f φ))
simp only [Set.preimage_setOf_eq, mem_setOf_eq, Formula.realize_relabel]