[Merged by Bors] - feat: tag IsInducing and Is{Open,Closed,}Embedding with fun_prop#29082
[Merged by Bors] - feat: tag IsInducing and Is{Open,Closed,}Embedding with fun_prop#29082grunweg wants to merge 2 commits intoleanprover-community:masterfrom
IsInducing and Is{Open,Closed,}Embedding with fun_prop#29082Conversation
PR summary e1f22205d3Import changes for modified filesNo significant changes to the import graph Import changes for all files
Declarations diffNo declarations were harmed in the making of this PR! 🐙 You can run this locally as follows## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>The doc-module for No changes to technical debt.You can run this locally as
|
|
maintainer merge? Looks reasonable to me, but I haven't used |
|
@jcommelin Did you mean to maintainer merge this? (That would have to go on a separate line; your comment did not have this effect.) |
IsInducing and Is{Open,Closed,}Embedding with fun_propIsInducing and Is{Open,Closed,}Embedding with fun_prop
ocfnash
left a comment
There was a problem hiding this comment.
Thanks, this is a good idea. Many more lemmas will need fun_prop added for this to be more useful but we have to start somewhere.
bors merge
| @[fun_prop] | ||
| protected lemma Topology.IsEmbedding.inclusion (h : s ⊆ t) : | ||
| IsEmbedding (inclusion h) := IsEmbedding.subtypeVal.codRestrict _ _ |
There was a problem hiding this comment.
For the sake of due diligence, I tested this one locally and I note that it works, but you do need to specify a discharger:
example {X : Type} [TopologicalSpace X] {s t : Set X} (h : s ⊆ t) :
Topology.IsEmbedding (Set.inclusion h) := by
fun_prop (disch := assumption)There was a problem hiding this comment.
A maybe nice feature one could ask for from fun_prop would be that it automatically attempts to discharge using any hypotheses already present in the goal.
#29082) I have not tested if this is usable in practice; perhaps it is not.
|
Pull request successfully merged into master. Build succeeded: |
IsInducing and Is{Open,Closed,}Embedding with fun_propIsInducing and Is{Open,Closed,}Embedding with fun_prop
leanprover-community#29082) I have not tested if this is usable in practice; perhaps it is not.
I have not tested if this is usable in practice; perhaps it is not.