![]() |
Mathbox for Thierry Arnoux |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > df-sigagen | Structured version Visualization version GIF version |
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.) |
Ref | Expression |
---|---|
df-sigagen | ⊢ sigaGen = (𝑥 ∈ V ↦ ∩ {𝑠 ∈ (sigAlgebra‘∪ 𝑥) ∣ 𝑥 ⊆ 𝑠}) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | csigagen 32777 | . 2 class sigaGen | |
2 | vx | . . 3 setvar 𝑥 | |
3 | cvv 3448 | . . 3 class V | |
4 | 2 | cv 1541 | . . . . . 6 class 𝑥 |
5 | vs | . . . . . . 7 setvar 𝑠 | |
6 | 5 | cv 1541 | . . . . . 6 class 𝑠 |
7 | 4, 6 | wss 3915 | . . . . 5 wff 𝑥 ⊆ 𝑠 |
8 | 4 | cuni 4870 | . . . . . 6 class ∪ 𝑥 |
9 | csiga 32747 | . . . . . 6 class sigAlgebra | |
10 | 8, 9 | cfv 6501 | . . . . 5 class (sigAlgebra‘∪ 𝑥) |
11 | 7, 5, 10 | crab 3410 | . . . 4 class {𝑠 ∈ (sigAlgebra‘∪ 𝑥) ∣ 𝑥 ⊆ 𝑠} |
12 | 11 | cint 4912 | . . 3 class ∩ {𝑠 ∈ (sigAlgebra‘∪ 𝑥) ∣ 𝑥 ⊆ 𝑠} |
13 | 2, 3, 12 | cmpt 5193 | . 2 class (𝑥 ∈ V ↦ ∩ {𝑠 ∈ (sigAlgebra‘∪ 𝑥) ∣ 𝑥 ⊆ 𝑠}) |
14 | 1, 13 | wceq 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 |