Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > ciun | GIF version |
Description: Extend class notation to include indexed union. Note: Historically (prior to 21-Oct-2005), set.mm used the notation ∪ 𝑥 ∈ 𝐴𝐵, with the same union symbol as cuni 3580. While that syntax was unambiguous, it did not allow for LALR parsing of the syntax constructions in set.mm. The new syntax uses as distinguished symbol ∪ instead of ∪ and does allow LALR parsing. Thanks to Peter Backes for suggesting this change. |
Ref | Expression |
---|---|
vx | setvar 𝑥 |
cA | class 𝐴 |
cB | class 𝐵 |
Ref | Expression |
---|---|
ciun | class ∪ 𝑥 ∈ 𝐴 𝐵 |
Colors of variables: wff set class |
Copyright terms: Public domain | W3C validator |