Theorems · Theorem · functional analysis

StarAlgebra.elemental.induction_on

∀ (R : Type u_1) {A : Type u_2} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : TopologicalSpace A]
  [inst_3 : Semiring A] [inst_4 : StarRing A] [inst_5 : IsSemitopologicalSemiring A] [inst_6 : ContinuousStar A]
  [inst_7 : Algebra R A] [inst_8 : StarModule R A] {x y : A} (hy : y ∈ StarAlgebra.elemental R x)
  {P : (u : A) → u ∈ StarAlgebra.elemental R x → Prop},
  P x ⋯ →
    P (star x) ⋯ →
      (∀ (r : R), P ((algebraMap R A) r) ⋯) →
        (∀ (u : A) (hu : u ∈ StarAlgebra.elemental R x) (v : A) (hv : v ∈ StarAlgebra.elemental R x),
            P u hu → P v hv → P (u + v) ⋯) →
          (∀ (u : A) (hu : u ∈ StarAlgebra.elemental R x) (v : A) (hv : v ∈ StarAlgebra.elemental R x),
              P u hu → P v hv → P (u * v) ⋯) →
            (∀ (s : Set A) (hs : s ⊆ ↑(StarAlgebra.elemental R x)),
                (∀ (u : A) (hu : u ∈ s), P u ⋯) → ∀ (v : A) (hv : v ∈ closure s), P v ⋯) →
              P y hy

Defined in

Mathlib.Topology.Algebra.StarSubalgebra

Cited by

0 results in Mathlib

Foundations

Depth 90 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommSemiringStarRingTopologicalSpaceSemiringStarRingIsSemitopologicalSemiringContinuousStarAlgebraStarModule