Closure and finiteness of SubMulAction and SubAddAction

def SubMulAction.closure (R : Type u_1) {M : Type u_2} [SMul R M] (s : Set M) : SubMulAction R M

The SubMulAction generated by a set s.

Equations

• SubMulAction.closure R s = sInf {p : SubMulAction R M | s ⊆ ↑p}

def SubAddAction.closure (R : Type u_1) {M : Type u_2} [VAdd R M] (s : Set M) : SubAddAction R M

The SubAddAction generated by a set s.

Equations

• SubAddAction.closure R s = sInf {p : SubAddAction R M | s ⊆ ↑p}

theorem SubMulAction.mem_closure {R : Type u_1} {M : Type u_2} [SMul R M] {s : Set M} {x : M} : x ∈ closure R s ↔ ∀ (p : SubMulAction R M), s ⊆ ↑p → x ∈ p

theorem SubAddAction.mem_closure {R : Type u_1} {M : Type u_2} [VAdd R M] {s : Set M} {x : M} : x ∈ closure R s ↔ ∀ (p : SubAddAction R M), s ⊆ ↑p → x ∈ p

theorem SubMulAction.subset_closure {R : Type u_1} {M : Type u_2} [SMul R M] {s : Set M} : s ⊆ ↑(closure R s)

theorem SubAddAction.subset_closure {R : Type u_1} {M : Type u_2} [VAdd R M] {s : Set M} : s ⊆ ↑(closure R s)

theorem SubMulAction.mem_closure_of_mem {R : Type u_1} {M : Type u_2} [SMul R M] {s : Set M} {x : M} (hx : x ∈ s) : x ∈ closure R s

theorem SubAddAction.mem_closure_of_mem {R : Type u_1} {M : Type u_2} [VAdd R M] {s : Set M} {x : M} (hx : x ∈ s) : x ∈ closure R s

theorem SubMulAction.closure_le {R : Type u_1} {M : Type u_2} [SMul R M] {s : Set M} {p : SubMulAction R M} : closure R s ≤ p ↔ s ⊆ ↑p

theorem SubAddAction.closure_le {R : Type u_1} {M : Type u_2} [VAdd R M] {s : Set M} {p : SubAddAction R M} : closure R s ≤ p ↔ s ⊆ ↑p

theorem SubMulAction.closure_mono {R : Type u_1} {M : Type u_2} [SMul R M] {s t : Set M} (h : s ⊆ t) : closure R s ≤ closure R t

theorem SubAddAction.closure_mono {R : Type u_1} {M : Type u_2} [VAdd R M] {s t : Set M} (h : s ⊆ t) : closure R s ≤ closure R t

def SubMulAction.FG {R : Type u_1} {M : Type u_2} [SMul R M] (p : SubMulAction R M) : Prop

A SubMulAction is finitely generated if it is the closure of a finite set.

Equations

• p.FG = ∃ (s : Set M), s.Finite ∧ p = SubMulAction.closure R s

def SubAddAction.FG {R : Type u_1} {M : Type u_2} [VAdd R M] (p : SubAddAction R M) : Prop

A SubAddAction is finitely generated if it is the closure of a finite set.

Equations

• p.FG = ∃ (s : Set M), s.Finite ∧ p = SubAddAction.closure R s

theorem SubMulAction.fg_iff {R : Type u_1} {M : Type u_2} [SMul R M] {p : SubMulAction R M} : p.FG ↔ ∃ (s : Finset M), p = closure R ↑s

theorem SubAddAction.fg_iff {R : Type u_1} {M : Type u_2} [VAdd R M] {p : SubAddAction R M} : p.FG ↔ ∃ (s : Finset M), p = closure R ↑s