Entry | Value |
---|---|
Name | subrelation_def |
Conclusion | !r s. subrelation r s <=> relation_to_set r SUBSET relation_to_set s |
Constructive Proof | Yes |
Axiom | N|A |
Classical Lemmas | N|A |
Constructive Lemmas | |
Contained Package | relation-def |
Comment | Standard HOL library retrieved from OpenTheory |