{"action":"created","issue":{"url":"https://api.github.com/repos/metamath/set.mm/issues/18","labels_url":"https://api.github.com/repos/metamath/set.mm/issues/18/labels{/name}","comments_url":"https://api.github.com/repos/metamath/set.mm/issues/18/comments","events_url":"https://api.github.com/repos/metamath/set.mm/issues/18/events","html_url":"https://github.com/metamath/set.mm/pull/18","id":116520403,"number":18,"title":"Transitive induction","user":{"login":"Drahflow","id":609223,"avatar_url":"https://avatars.githubusercontent.com/u/609223?v=3","gravatar_id":"","url":"https://api.github.com/users/Drahflow","html_url":"https://github.com/Drahflow","followers_url":"https://api.github.com/users/Drahflow/followers","following_url":"https://api.github.com/users/Drahflow/following{/other_user}","gists_url":"https://api.github.com/users/Drahflow/gists{/gist_id}","starred_url":"https://api.github.com/users/Drahflow/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/Drahflow/subscriptions","organizations_url":"https://api.github.com/users/Drahflow/orgs","repos_url":"https://api.github.com/users/Drahflow/repos","events_url":"https://api.github.com/users/Drahflow/events{/privacy}","received_events_url":"https://api.github.com/users/Drahflow/received_events","type":"User","site_admin":false},"labels":[],"state":"closed","locked":false,"assignee":null,"milestone":null,"comments":5,"created_at":"2015-11-12T10:24:35Z","updated_at":"2015-11-30T04:56:00Z","closed_at":"2015-11-28T03:27:32Z","pull_request":{"url":"https://api.github.com/repos/metamath/set.mm/pulls/18","html_url":"https://github.com/metamath/set.mm/pull/18","diff_url":"https://github.com/metamath/set.mm/pull/18.diff","patch_url":"https://github.com/metamath/set.mm/pull/18.patch"},"body":"Revised version of #17, now against develop branch."},"comment":{"url":"https://api.github.com/repos/metamath/set.mm/issues/comments/160515835","html_url":"https://github.com/metamath/set.mm/pull/18#issuecomment-160515835","issue_url":"https://api.github.com/repos/metamath/set.mm/issues/18","id":160515835,"user":{"login":"digama0","id":868588,"avatar_url":"https://avatars.githubusercontent.com/u/868588?v=3","gravatar_id":"","url":"https://api.github.com/users/digama0","html_url":"https://github.com/digama0","followers_url":"https://api.github.com/users/digama0/followers","following_url":"https://api.github.com/users/digama0/following{/other_user}","gists_url":"https://api.github.com/users/digama0/gists{/gist_id}","starred_url":"https://api.github.com/users/digama0/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/digama0/subscriptions","organizations_url":"https://api.github.com/users/digama0/orgs","repos_url":"https://api.github.com/users/digama0/repos","events_url":"https://api.github.com/users/digama0/events{/privacy}","received_events_url":"https://api.github.com/users/digama0/received_events","type":"User","site_admin":false},"created_at":"2015-11-30T04:56:00Z","updated_at":"2015-11-30T04:56:00Z","body":"No, what I defined was a very particular case of ^r with explicit base set where B is (Base`K) and R is the covering relation in a lattice, ( <o ` K ). I did not attempt to define the general notion as you have done. It's just that I find myself doing a lot of similar theorems to what you have, but it isn't as simple as just importing your version and retrofitting my theorems because of the explicit base set thing. It's not essential for my work to have the general definition (I will just have these repeated theorems in the present version) but I figure that if you are working on a generalization than it should be general enough to handle all cases that might appear in set.mm, which is why I mentioned it."}}