L : Language
M : Type w
N : Type ?u.37249
P : Type ?u.37252
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
s✝ : Set M
p : M → Prop
x : M
s : Set M
hs : LowerAdjoint.toFun (closure L) s = ⊤
Hs : ∀ (x : M), x ∈ s → p x
Hfun : ∀ {n : ℕ} (f : Functions L n), ClosedUnder f (setOf p)
this : ∀ (x : M), x ∈ LowerAdjoint.toFun (closure L) s → p x
⊢ p x
L : Language
M : Type w
N : Type ?u.37249
P : Type ?u.37252
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
s✝ : Set M
p : M → Prop
x : M
s : Set M
hs : LowerAdjoint.toFun (closure L) s = ⊤
Hs : ∀ (x : M), x ∈ s → p x
Hfun : ∀ {n : ℕ} (f : Functions L n), ClosedUnder f (setOf p)
⊢ p x
have : ∀ x ∈ closure L s, p x := fun x hx => closure_induction hx Hs fun {n} => Hfun
no goals
L : Language
M : Type w
N : Type ?u.37249
P : Type ?u.37252
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
s✝ : Set M
p : M → Prop
x : M
s : Set M
hs : LowerAdjoint.toFun (closure L) s = ⊤
Hs : ∀ (x : M), x ∈ s → p x
Hfun : ∀ {n : ℕ} (f : Functions L n), ClosedUnder f (setOf p)
this : ∀ (x : M), x ∈ LowerAdjoint.toFun (closure L) s → p x
⊢ p x
simpa [hs] using this x