L : Language
M : Type w
N : Type ?u.35964
P : Type ?u.35967
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
S : Substructure L M
s : Set M
inst✝ : Countable ((l : ℕ) × Functions L l)
h : Set.Countable s
this : Countable ↑s
⊢ Countable { x // x ∈ LowerAdjoint.toFun (closure L) s }
L : Language
M : Type w
N : Type ?u.35964
P : Type ?u.35967
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
S : Substructure L M
s : Set M
inst✝ : Countable ((l : ℕ) × Functions L l)
h : Set.Countable s
⊢ Countable { x // x ∈ LowerAdjoint.toFun (closure L) s }
haveI : Countable s := h.to_subtype
L : Language
M : Type w
N : Type ?u.35964
P : Type ?u.35967
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
S : Substructure L M
s : Set M
inst✝ : Countable ((l : ℕ) × Functions L l)
h : Set.Countable s
this : Countable ↑s
⊢ lift (#{ x // x ∈ LowerAdjoint.toFun (closure L) s }) ≤ ℵ₀
L : Language
M : Type w
N : Type ?u.35964
P : Type ?u.35967
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
S : Substructure L M
s : Set M
inst✝ : Countable ((l : ℕ) × Functions L l)
h : Set.Countable s
this : Countable ↑s
⊢ Countable { x // x ∈ LowerAdjoint.toFun (closure L) s }
rw [← mk_le_aleph0_iff, ← lift_le_aleph0]
no goals
L : Language
M : Type w
N : Type ?u.35964
P : Type ?u.35967
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
S : Substructure L M
s : Set M
inst✝ : Countable ((l : ℕ) × Functions L l)
h : Set.Countable s
this : Countable ↑s
⊢ lift (#{ x // x ∈ LowerAdjoint.toFun (closure L) s }) ≤ ℵ₀
exact lift_card_closure_le_card_term.trans mk_le_aleph0