L : Language
M : Type u_3
inst✝¹ : Structure L M
inst✝ : Countable ((l : ℕ) × Functions L l)
s : Substructure L M
⊢ CG s → Countable { x // x ∈ s }
L : Language
M : Type u_3
inst✝¹ : Structure L M
inst✝ : Countable ((l : ℕ) × Functions L l)
s : Substructure L M
⊢ CG s ↔ Countable { x // x ∈ s }
refine' ⟨_, fun h => ⟨s, h.to_set, s.closure_eq⟩⟩
case intro.intro
L : Language
M : Type u_3
inst✝¹ : Structure L M
inst✝ : Countable ((l : ℕ) × Functions L l)
s : Set M
h : Set.Countable s
⊢ Countable { x // x ∈ LowerAdjoint.toFun (closure L) s }
L : Language
M : Type u_3
inst✝¹ : Structure L M
inst✝ : Countable ((l : ℕ) × Functions L l)
s : Substructure L M
⊢ CG s → Countable { x // x ∈ s }
rintro ⟨s, h, rfl⟩
no goals
case intro.intro
L : Language
M : Type u_3
inst✝¹ : Structure L M
inst✝ : Countable ((l : ℕ) × Functions L l)
s : Set M
h : Set.Countable s
⊢ Countable { x // x ∈ LowerAdjoint.toFun (closure L) s }
exact h.substructure_closure L