L : Language
M : Type w
N : Type ?u.683008
P : Type ?u.683011
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
A s : Set M
h : A ⊆ ↑S
⊢ withConstants (LowerAdjoint.toFun (closure L) (A ∪ s)) (_ : A ⊆ ↑(LowerAdjoint.toFun (closure L) (A ∪ s))) ≤
    LowerAdjoint.toFun (closure (L[[↑A]])) s
L : Language
M : Type w
N : Type ?u.683008
P : Type ?u.683011
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
A s : Set M
h : A ⊆ ↑S
⊢ LowerAdjoint.toFun (closure (L[[↑A]])) s =
    withConstants (LowerAdjoint.toFun (closure L) (A ∪ s)) (_ : A ⊆ ↑(LowerAdjoint.toFun (closure L) (A ∪ s)))
refine' closure_eq_of_le ((A.subset_union_right s).trans subset_closure) _
L : Language
M : Type w
N : Type ?u.683008
P : Type ?u.683011
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
A s : Set M
h : A ⊆ ↑S
⊢ ↑(LHom.substructureReduct (lhomWithConstants L ↑A))
      (withConstants (LowerAdjoint.toFun (closure L) (A ∪ s)) (_ : A ⊆ ↑(LowerAdjoint.toFun (closure L) (A ∪ s)))) ≤
    ↑(LHom.substructureReduct (lhomWithConstants L ↑A)) (LowerAdjoint.toFun (closure (L[[↑A]])) s)
L : Language
M : Type w
N : Type ?u.683008
P : Type ?u.683011
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
A s : Set M
h : A ⊆ ↑S
⊢ withConstants (LowerAdjoint.toFun (closure L) (A ∪ s)) (_ : A ⊆ ↑(LowerAdjoint.toFun (closure L) (A ∪ s))) ≤
    LowerAdjoint.toFun (closure (L[[↑A]])) s
rw [← (L.lhomWithConstants A).substructureReduct.le_iff_le]
L : Language
M : Type w
N : Type ?u.683008
P : Type ?u.683011
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
A s : Set M
h : A ⊆ ↑S
⊢ A ⊆ ↑(LowerAdjoint.toFun (closure (L[[↑A]])) s)
L : Language
M : Type w
N : Type ?u.683008
P : Type ?u.683011
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
A s : Set M
h : A ⊆ ↑S
⊢ ↑(LHom.substructureReduct (lhomWithConstants L ↑A))
      (withConstants (LowerAdjoint.toFun (closure L) (A ∪ s)) (_ : A ⊆ ↑(LowerAdjoint.toFun (closure L) (A ∪ s)))) ≤
    ↑(LHom.substructureReduct (lhomWithConstants L ↑A)) (LowerAdjoint.toFun (closure (L[[↑A]])) s)
simp only [subset_closure, reduct_withConstants, closure_le, LHom.coe_substructureReduct,
  Set.union_subset_iff, and_true_iff]
no goals
L : Language
M : Type w
N : Type ?u.683008
P : Type ?u.683011
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
A s : Set M
h : A ⊆ ↑S
⊢ A ⊆ ↑(LowerAdjoint.toFun (closure (L[[↑A]])) s)
exact subset_closure_withConstants