structure CommSemigroup.Ideal (A : Type u_1) [CommSemigroup A] : Type u_1

• carrier : Set A
• is_ideal (a b : A) : a ∈ self.carrier → a * b ∈ self.carrier

instance CommSemigroup.Ideal.instSetLike {A : Type u_1} [CommSemigroup A] : SetLike (CommSemigroup.Ideal A) A

Equations

• CommSemigroup.Ideal.instSetLike = { coe := fun (a : CommSemigroup.Ideal A) => a.carrier, coe_injective' := ⋯ }

theorem CommSemigroup.Ideal.mul_mem_left {A : Type u_1} [CommSemigroup A] (I : CommSemigroup.Ideal A) {a : A} (ha : a ∈ I) (b : A) : a * b ∈ I

theorem CommSemigroup.Ideal.mul_mem_right {A : Type u_1} [CommSemigroup A] (I : CommSemigroup.Ideal A) (a : A) {b : A} (hb : b ∈ I) : a * b ∈ I

instance CommSemigroup.Ideal.instMulMemClass {A : Type u_1} [CommSemigroup A] : MulMemClass (CommSemigroup.Ideal A) A

def CommSemigroup.Ideal.asSubsemigroup {A : Type u_1} [CommSemigroup A] (I : CommSemigroup.Ideal A) : Subsemigroup A

Equations

• I.asSubsemigroup = { carrier := ↑I, mul_mem' := ⋯ }

theorem CommSemigroup.Ideal.le_iff {A : Type u_1} [CommSemigroup A] {I J : CommSemigroup.Ideal A} : I ≤ J ↔ ↑I ⊆ ↑J

instance CommSemigroup.Ideal.instMax {A : Type u_1} [CommSemigroup A] : Max (CommSemigroup.Ideal A)

Equations

• CommSemigroup.Ideal.instMax = { max := fun (I J : CommSemigroup.Ideal A) => { carrier := ↑I ∪ ↑J, is_ideal := ⋯ } }

@[simp]

theorem CommSemigroup.Ideal.coe_sup {A : Type u_1} [CommSemigroup A] (I J : CommSemigroup.Ideal A) : ↑(I ⊔ J) = ↑I ∪ ↑J

theorem CommSemigroup.Ideal.mem_sup {A : Type u_1} [CommSemigroup A] {I J : CommSemigroup.Ideal A} {x : A} : x ∈ I ⊔ J ↔ x ∈ I ∨ x ∈ J

instance CommSemigroup.Ideal.instMin {A : Type u_1} [CommSemigroup A] : Min (CommSemigroup.Ideal A)

Equations

• CommSemigroup.Ideal.instMin = { min := fun (I J : CommSemigroup.Ideal A) => { carrier := ↑I ∩ ↑J, is_ideal := ⋯ } }

@[simp]

theorem CommSemigroup.Ideal.coe_inf {A : Type u_1} [CommSemigroup A] (I J : CommSemigroup.Ideal A) : ↑(I ⊓ J) = ↑I ∩ ↑J

theorem CommSemigroup.Ideal.mem_inf {A : Type u_1} [CommSemigroup A] {I J : CommSemigroup.Ideal A} {x : A} : x ∈ I ⊓ J ↔ x ∈ I ∧ x ∈ J

instance CommSemigroup.Ideal.instSemilatticeSup {A : Type u_1} [CommSemigroup A] : SemilatticeSup (CommSemigroup.Ideal A)

Equations

• CommSemigroup.Ideal.instSemilatticeSup = SemilatticeSup.mk (fun (a b : CommSemigroup.Ideal A) => a ⊔ b) ⋯ ⋯ ⋯

instance CommSemigroup.Ideal.instSemilatticeInf {A : Type u_1} [CommSemigroup A] : SemilatticeInf (CommSemigroup.Ideal A)

Equations

• CommSemigroup.Ideal.instSemilatticeInf = SemilatticeInf.mk (fun (a b : CommSemigroup.Ideal A) => a ⊓ b) ⋯ ⋯ ⋯

instance CommSemigroup.Ideal.instSupSet {A : Type u_1} [CommSemigroup A] : SupSet (CommSemigroup.Ideal A)

Equations

• CommSemigroup.Ideal.instSupSet = { sSup := fun (S : Set (CommSemigroup.Ideal A)) => { carrier := ⋃ I ∈ S, ↑I, is_ideal := ⋯ } }

@[simp]

theorem CommSemigroup.Ideal.coe_sSup {A : Type u_1} [CommSemigroup A] (S : Set (CommSemigroup.Ideal A)) : ↑(sSup S) = ⋃ I ∈ S, ↑I

theorem CommSemigroup.Ideal.mem_sSup {A : Type u_1} [CommSemigroup A] {S : Set (CommSemigroup.Ideal A)} {x : A} : x ∈ sSup S ↔ ∃ I ∈ S, x ∈ ↑I

@[simp]

theorem CommSemigroup.Ideal.coe_biSup {A : Type u_1} [CommSemigroup A] (S : Set (CommSemigroup.Ideal A)) : ↑(⨆ I ∈ S, I) = ⋃ I ∈ S, ↑I

theorem CommSemigroup.Ideal.mem_biSup {A : Type u_1} [CommSemigroup A] {S : Set (CommSemigroup.Ideal A)} {x : A} : x ∈ ⨆ I ∈ S, I ↔ ∃ I ∈ S, x ∈ ↑I

@[simp]

theorem CommSemigroup.Ideal.coe_iSup {A : Type u_1} [CommSemigroup A] {ι : Type u_2} (f : ι → CommSemigroup.Ideal A) : ↑(⨆ (i : ι), f i) = ⋃ (i : ι), ↑(f i)

theorem CommSemigroup.Ideal.mem_iSup {A : Type u_1} [CommSemigroup A] {ι : Type u_2} {f : ι → CommSemigroup.Ideal A} {x : A} : x ∈ ⨆ (i : ι), f i ↔ ∃ (i : ι), x ∈ f i

instance CommSemigroup.Ideal.instInfSet {A : Type u_1} [CommSemigroup A] : InfSet (CommSemigroup.Ideal A)

Equations

• CommSemigroup.Ideal.instInfSet = { sInf := fun (S : Set (CommSemigroup.Ideal A)) => { carrier := ⋂ I ∈ S, ↑I, is_ideal := ⋯ } }

@[simp]

theorem CommSemigroup.Ideal.coe_sInf {A : Type u_1} [CommSemigroup A] (S : Set (CommSemigroup.Ideal A)) : ↑(sInf S) = ⋂ I ∈ S, ↑I

theorem CommSemigroup.Ideal.mem_sInf {A : Type u_1} [CommSemigroup A] {S : Set (CommSemigroup.Ideal A)} {x : A} : x ∈ sInf S ↔ ∀ I ∈ S, x ∈ ↑I

@[simp]

theorem CommSemigroup.Ideal.coe_biInf {A : Type u_1} [CommSemigroup A] (S : Set (CommSemigroup.Ideal A)) : ↑(⨅ I ∈ S, I) = ⋂ I ∈ S, ↑I

theorem CommSemigroup.Ideal.mem_biInf {A : Type u_1} [CommSemigroup A] {S : Set (CommSemigroup.Ideal A)} {x : A} : x ∈ ⨅ I ∈ S, I ↔ ∀ I ∈ S, x ∈ ↑I

@[simp]

theorem CommSemigroup.Ideal.coe_iInf {A : Type u_1} [CommSemigroup A] {ι : Type u_2} (f : ι → CommSemigroup.Ideal A) : ↑(⨅ (i : ι), f i) = ⋂ (i : ι), ↑(f i)

theorem CommSemigroup.Ideal.mem_iInf {A : Type u_1} [CommSemigroup A] {ι : Type u_2} {f : ι → CommSemigroup.Ideal A} {x : A} : x ∈ ⨅ (i : ι), f i ↔ ∀ (i : ι), x ∈ f i

instance CommSemigroup.Ideal.instCompleteSemilatticeSup {A : Type u_1} [CommSemigroup A] : CompleteSemilatticeSup (CommSemigroup.Ideal A)

Equations

• CommSemigroup.Ideal.instCompleteSemilatticeSup = CompleteSemilatticeSup.mk ⋯ ⋯

instance CommSemigroup.Ideal.instCompleteSemilatticeInf {A : Type u_1} [CommSemigroup A] : CompleteSemilatticeInf (CommSemigroup.Ideal A)

Equations

• CommSemigroup.Ideal.instCompleteSemilatticeInf = CompleteSemilatticeInf.mk ⋯ ⋯

instance CommSemigroup.Ideal.instLattice {A : Type u_1} [CommSemigroup A] : Lattice (CommSemigroup.Ideal A)

Equations

• CommSemigroup.Ideal.instLattice = Lattice.mk SemilatticeInf.inf ⋯ ⋯ ⋯

instance CommSemigroup.Ideal.instTop {A : Type u_1} [CommSemigroup A] : Top (CommSemigroup.Ideal A)

Equations

• CommSemigroup.Ideal.instTop = { top := { carrier := Set.univ, is_ideal := ⋯ } }

@[simp]

theorem CommSemigroup.Ideal.coe_top {A : Type u_1} [CommSemigroup A] : ↑⊤ = Set.univ

theorem CommSemigroup.Ideal.mem_top {A : Type u_1} [CommSemigroup A] (x : A) : x ∈ ⊤

@[simp]

theorem CommSemigroup.Ideal.mem_top_iff_true {A : Type u_1} [CommSemigroup A] (x : A) : x ∈ ⊤ ↔ True

instance CommSemigroup.Ideal.instBot {A : Type u_1} [CommSemigroup A] : Bot (CommSemigroup.Ideal A)

Equations

• CommSemigroup.Ideal.instBot = { bot := { carrier := ∅, is_ideal := ⋯ } }

@[simp]

theorem CommSemigroup.Ideal.coe_bot {A : Type u_1} [CommSemigroup A] : ↑⊥ = ∅

theorem CommSemigroup.Ideal.not_mem_bot {A : Type u_1} [CommSemigroup A] (x : A) : x ∉ ⊥

@[simp]

theorem CommSemigroup.Ideal.mem_bot_iff_false {A : Type u_1} [CommSemigroup A] (x : A) : x ∈ ⊥ ↔ False

instance CommSemigroup.Ideal.instCompleteLattice {A : Type u_1} [CommSemigroup A] : CompleteLattice (CommSemigroup.Ideal A)

Equations

• CommSemigroup.Ideal.instCompleteLattice = CompleteLattice.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

def CommSemigroup.Ideal.closure {A : Type u_1} [CommSemigroup A] (s : Set A) : CommSemigroup.Ideal A

Equations

• CommSemigroup.Ideal.closure s = sInf {I : CommSemigroup.Ideal A | s ⊆ ↑I}

theorem CommSemigroup.Ideal.closure_eq_sInf {A : Type u_1} [CommSemigroup A] (s : Set A) : CommSemigroup.Ideal.closure s = sInf {I : CommSemigroup.Ideal A | s ⊆ ↑I}

theorem CommSemigroup.Ideal.subset_closure {A : Type u_1} [CommSemigroup A] (s : Set A) : s ⊆ ↑(CommSemigroup.Ideal.closure s)

theorem CommSemigroup.Ideal.closure_eq {A : Type u_1} [CommSemigroup A] (s : Set A) : CommSemigroup.Ideal.closure s = { carrier := s ∪ s * Set.univ, is_ideal := ⋯ }

theorem CommSemigroup.Ideal.closure_induction {A : Type u_1} [CommSemigroup A] {s : Set A} {p : A → Prop} (basic : ∀ x ∈ s, p x) (ideal : ∀ (x y : A), x ∈ s → p x → p (x * y)) (x : A) : x ∈ CommSemigroup.Ideal.closure s → p x

theorem CommSemigroup.Ideal.closure_induction' {A : Type u_1} [CommSemigroup A] {s : Set A} {p : (a : A) → a ∈ CommSemigroup.Ideal.closure s → Prop} (basic : ∀ (x : A) (h : x ∈ s), p x ⋯) (ideal : ∀ (x y : A) (h : x ∈ s), p x ⋯ → p (x * y) ⋯) (x : A) (h : x ∈ CommSemigroup.Ideal.closure s) : p x h

theorem CommSemigroup.Ideal.mem_closure {A : Type u_1} [CommSemigroup A] {s : Set A} {x : A} : x ∈ CommSemigroup.Ideal.closure s ↔ x ∈ s ∪ s * Set.univ