M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type ?u.8472
B : Set M
s : Set (α → M)
hAs : Definable ∅ (L[[↑A]]) s
hAB : A ⊆ B
⊢ Definable ∅ (L[[↑B]]) s
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type ?u.8472
B : Set M
s : Set (α → M)
hAs : Definable A L s
hAB : A ⊆ B
⊢ Definable B L s
rw [definable_iff_empty_definable_with_params] at *
no goals
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type ?u.8472
B : Set M
s : Set (α → M)
hAs : Definable ∅ (L[[↑A]]) s
hAB : A ⊆ B
⊢ Definable ∅ (L[[↑B]]) s
exact hAs.map_expansion (L.lhomWithConstantsMap (Set.inclusion hAB))