L : Language
M : Type w
N : Type ?u.34936
P : Type ?u.34939
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
s : Set M
⊢ lift (#{ x // x ∈ LowerAdjoint.toFun (closure L) s }) ≤ max ℵ₀ (lift (#↑s) + lift (#(i : ℕ) × Functions L i))
L : Language
M : Type w
N : Type ?u.34936
P : Type ?u.34939
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
s : Set M
⊢ lift (#{ x // x ∈ LowerAdjoint.toFun (closure L) s }) ≤ max ℵ₀ (lift (#↑s) + lift (#(i : ℕ) × Functions L i))
rw [← lift_umax]
L : Language
M : Type w
N : Type ?u.34936
P : Type ?u.34939
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
s : Set M
⊢ max ℵ₀ (#↑s ⊕ (i : ℕ) × Functions L i) ≤ max ℵ₀ (lift (#↑s) + lift (#(i : ℕ) × Functions L i))
L : Language
M : Type w
N : Type ?u.34936
P : Type ?u.34939
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
s : Set M
⊢ lift (#{ x // x ∈ LowerAdjoint.toFun (closure L) s }) ≤ max ℵ₀ (lift (#↑s) + lift (#(i : ℕ) × Functions L i))
refine' lift_card_closure_le_card_term.trans (Term.card_le.trans _)
no goals
L : Language
M : Type w
N : Type ?u.34936
P : Type ?u.34939
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
S : Substructure L M
s : Set M
⊢ max ℵ₀ (#↑s ⊕ (i : ℕ) × Functions L i) ≤ max ℵ₀ (lift (#↑s) + lift (#(i : ℕ) × Functions L i))
rw [mk_sum, lift_umax.{w, u}]