feat(set_theory/zfc/basic): tweak of_Set and to_Set
#18694
Conversation
vihdzp
added
the
awaiting-review
| @@ -1095,7 +1092,7 @@ mem_univ.2 $ or.elim (classical.em $ ∃ x, ∀ y, A y ↔ y = x) | |||
| (λ hn, ⟨∅, ext (λ z, coe_empty.symm ▸ ⟨false.rec _, λ ⟨._, ⟨x, rfl, H⟩, zA⟩, hn ⟨x, H⟩⟩)⟩) | |||
|
|
|||
| /-- Function value -/ | |||
| def fval (F A : Class.{u}) : Class.{u} := iota (λ y, to_Set (λ x, F (Set.pair x y)) A) | |||
| def fval (F A : Class.{u}) : Class.{u} := iota $ λ y, Class.has_mem.mem A $ λ x, F (Set.pair x y) | |||
There was a problem hiding this comment.
Hmm, this feels pretty weird. Do we not have syntax to construct a Class from a lambda?
There was a problem hiding this comment.
Perhaps
| def fval (F A : Class.{u}) : Class.{u} := iota $ λ y, Class.has_mem.mem A $ λ x, F (Set.pair x y) | |
| def fval (F A : Class.{u}) : Class.{u} := iota $ λ y, A ∈ ({x | F (Set.pair x y)} : Class) |
There was a problem hiding this comment.
This isn't able to find the ∈ instance, since the instance searcher can't see through the def-eq set Set = Class.
There was a problem hiding this comment.
We don't have special syntax to construct classes, I'm afraid. We probably should though, this reminds me of the situation with matrix.of.
I'll add this after the file is ported.
| /-- Assert that `A` is a ZFC set satisfying `B` -/ | ||
| def to_Set (B : Class.{u}) (A : Class.{u}) : Prop := ∃ x, ↑x = A ∧ B x |
There was a problem hiding this comment.
Based on @digama0's comments on Zulip it sounds like they would prefer to keep this; and I certainly trust their judgement over my own.
So I don't think this PR is going anywhere unless Mario both finds time to review this, and can also be persuaded of the change.
There was a problem hiding this comment.
To add to the statements made on Zulip, I'm fairly sure that this is one of the constructors used in the metamath -> lean translation, so I would prefer to keep of_Set and to_Set as is, potential almost-duplication notwithstanding. The definitions are all trivial, so refactoring them doesn't gain us much in terms of shortened proofs but the type signatures are important. I think this is best revisited after the port.
|
I still have more to say on this topic, but I agree with postponing it until the port. |
We rename some things to better fit general Mathlib convention. In summary, we:
Class.of_SettoClass.coeof_Set.injtocoe_injective, addcoe_injClass.to_Set, as it's identical toClass.memWill be ported to Lean 4 along with the rest of the file here: leanprover-community/mathlib4#3165