M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type ?u.1235
B : Set M
s : Set (α → M)
⊢ (∃ φ, s = setOf (Formula.Realize φ)) ↔
    ∃ b, s = setOf (Formula.Realize (↑(LEquiv.onFormula (LEquiv.addEmptyConstants L ↑∅)).symm b))
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type ?u.1235
B : Set M
s : Set (α → M)
⊢ Definable ∅ L s ↔ ∃ φ, s = setOf (Formula.Realize φ)
rw [Definable, Equiv.exists_congr_left (LEquiv.addEmptyConstants L (∅ : Set M)).onFormula]
no goals
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type ?u.1235
B : Set M
s : Set (α → M)
⊢ (∃ φ, s = setOf (Formula.Realize φ)) ↔
    ∃ b, s = setOf (Formula.Realize (↑(LEquiv.onFormula (LEquiv.addEmptyConstants L ↑∅)).symm b))
simp [-constantsOn]