Nearby theorems
|
|
brismu bridi |
< Previous
Next >
Nearby theorems |
|
| Mirrors > Home > Home > Th. List > df-gripau | |||
| Description: Definition of {gripau} in terms of {cmima} and {na.a}. Defined in section 7 of [CLL] p. 18 based on the gloss "set-part". This definition is phrased with an implicit universal quantification instead of {ro da zo'u da cmima ko'a na.a ko'e} or {ro da poi ke'a cmima ko'a ku'o zo'u da cmima ko'e} for succinctness and ease of theorem-proving. |
| Ref | Expression |
|---|---|
| df-gripau | ⊢ go ko'a gripau ko'e gi ko'i cmima ko'a na.a ko'e |
| Copyright terms: Public domain | W3C validator |