Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-sigagen Structured version   Visualization version   GIF version

Definition df-sigagen 32778
Description: Define the sigma-algebra generated by a given collection of sets as the intersection of all sigma-algebra containing that set. (Contributed by Thierry Arnoux, 27-Dec-2016.)
Assertion
Ref Expression
df-sigagen sigaGen = (𝑥 ∈ V ↦ {𝑠 ∈ (sigAlgebra‘ 𝑥) ∣ 𝑥𝑠})
Distinct variable group:   𝑥,𝑠

Detailed syntax breakdown of Definition df-sigagen
StepHypRef Expression
1 csigagen 32777 . 2 class sigaGen
2 vx . . 3 setvar 𝑥
3 cvv 3448 . . 3 class V
42cv 1541 . . . . . 6 class 𝑥
5 vs . . . . . . 7 setvar 𝑠
65cv 1541 . . . . . 6 class 𝑠
74, 6wss 3915 . . . . 5 wff 𝑥𝑠
84cuni 4870 . . . . . 6 class 𝑥
9 csiga 32747 . . . . . 6 class sigAlgebra
108, 9cfv 6501 . . . . 5 class (sigAlgebra‘ 𝑥)
117, 5, 10crab 3410 . . . 4 class {𝑠 ∈ (sigAlgebra‘ 𝑥) ∣ 𝑥𝑠}
1211cint 4912 . . 3 class {𝑠 ∈ (sigAlgebra‘ 𝑥) ∣ 𝑥𝑠}
132, 3, 12cmpt 5193 . 2 class (𝑥 ∈ V ↦ {𝑠 ∈ (sigAlgebra‘ 𝑥) ∣ 𝑥𝑠})
141, 13wceq 1542 1 wff sigaGen = (𝑥 ∈ V ↦ {𝑠 ∈ (sigAlgebra‘ 𝑥) ∣ 𝑥𝑠})
Colors of variables: wff setvar class
This definition is referenced by:  sigagenval  32779  dmsigagen  32783  brsiga  32822
  Copyright terms: Public domain W3C validator