pi.star_ordered_ring

This file contains the definition of pi.star_ordered_ring.

def Set.ofPi {ι : Type u_1} {B : ι → Type u_2} [DecidableEq ι] [(i : ι) → Zero (B i)] (s : Set ((i : ι) → B i)) (i : ι) : Set (B i)

Coordinate projection of a set of dependent functions along Pi.single.

Equations

• s.ofPi i x = (Pi.single i x ∈ s)

theorem Set.piOfPi {ι : Type u_1} {B : ι → Type u_2} [DecidableEq ι] [(i : ι) → AddZeroClass (B i)] {s : (i : ι) → Set (B i)} (h : ∀ (i : ι), s i 0) : (univ.pi s).ofPi = s

def AddSubmonoid.ofPi {ι : Type u_1} {B : ι → Type u_2} [DecidableEq ι] [(i : ι) → AddZeroClass (B i)] : AddSubmonoid ((i : ι) → B i) → (i : ι) → AddSubmonoid (B i)

Coordinate projection of an additive submonoid of dependent functions along Pi.single.

Equations

• h.ofPi i = { carrier := fun (x : B i) => x ∈ h.carrier.ofPi i, add_mem' := ⋯, zero_mem' := ⋯ }

theorem AddSubmonoid.piOfPi {ι : Type u_1} {B : ι → Type u_2} [DecidableEq ι] [(i : ι) → AddZeroClass (B i)] (h : (i : ι) → AddSubmonoid (B i)) : (pi Set.univ h).ofPi = h

theorem Set.ofPi_mem' {ι : Type u_1} {B : ι → Type u_2} [DecidableEq ι] [(i : ι) → AddZeroClass (B i)] {s : (i : ι) → Set (B i)} {S : Set ((i : ι) → B i)} (hs : univ.pi s ⊆ S) (h : ∀ (i : ι), s i 0) (i : ι) : s i ⊆ S.ofPi i

theorem AddSubmonoid.mem_closure_pi {ι : Type u_1} {B : ι → Type u_2} [(i : ι) → AddZeroClass (B i)] {s : (i : ι) → Set (B i)} {x : (i : ι) → B i} : x ∈ closure (Set.univ.pi fun (i : ι) => s i) → ∀ (i : ι), x i ∈ closure (s i)

theorem Pi.StarOrderedRing.nonneg_def {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → NonUnitalSemiring (α i)] [(i : ι) → PartialOrder (α i)] [(i : ι) → StarRing (α i)] [∀ (i : ι), StarOrderedRing (α i)] (h : ∀ (i : ι) (x : α i), 0 ≤ x ↔ ∃ (y : α i), star y * y = x) (x : (i : ι) → α i) : 0 ≤ x ↔ ∃ (y : (i : ι) → α i), star y * y = x

instance instCovariantClassForallSwapHAddLeOfStarOrderedRing_leanPool {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Ring (α i)] [(i : ι) → PartialOrder (α i)] [(i : ι) → StarRing (α i)] [∀ (i : ι), StarOrderedRing (α i)] : CovariantClass ((i : ι) → α i) ((i : ι) → α i) (Function.swap fun (x x_1 : (i : ι) → α i) => x + x_1) fun (x x_1 : (i : ι) → α i) => x ≤ x_1

theorem Pi.StarOrderedRing.le_def {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Ring (α i)] [(i : ι) → PartialOrder (α i)] [(i : ι) → StarRing (α i)] [∀ (i : ι), StarOrderedRing (α i)] (h : ∀ (i : ι) (x : α i), 0 ≤ x ↔ ∃ (y : α i), star y * y = x) (x y : (i : ι) → α i) : x ≤ y ↔ ∃ (z : (i : ι) → α i), star z * z = y - x

theorem Pi.starOrderedRing {ι : Type u_1} {B : ι → Type u_2} [(i : ι) → Ring (B i)] [(i : ι) → PartialOrder (B i)] [(i : ι) → StarRing (B i)] [∀ (i : ι), StarOrderedRing (B i)] (h : ∀ (i : ι) (x : B i), 0 ≤ x ↔ ∃ (y : B i), star y * y = x) : StarOrderedRing ((i : ι) → B i)

Dependent functions over star-ordered rings are star-ordered coordinatewise.