Set.image2_def
theorem Set.image2_def :
∀ {α β γ : Type u} (f : α → β → γ) (s : Set α) (t : Set β), Set.image2 f s t = Seq.seq (f <$> s) fun x => t := by
sorry
The theorem `Set.image2_def` asserts that, for any types `α`, `β`, and `γ`, and any binary function `f : α → β → γ`, the image of this function with respect to sets `s : Set α` and `t : Set β` can be expressed in terms of monadic operations. Specifically, it says that `Set.image2 f s t` is equal to the sequence operation performed on the function `f` mapped over the set `s` and a unit function of `t`. This establishes a connection between the image of a binary function over two sets and sequence operations in a monad. However, this theorem cannot be used as the definition of `Set.image2` due to the lack of universe polymorphism in Lean.
More concisely: The theorem `Set.image2_def` states that for any types `α`, `β`, and `γ`, and any binary function `f : α → β → γ`, the image of `f` over sets `s : Set α` and `t : Set β` is equal to the sequence operation applied to `f` over `s` and the unit function of `t`.
|
Set.coe_eq_image_val
theorem Set.coe_eq_image_val : ∀ {α : Type u} {s : Set α} (t : Set ↑s), Lean.Internal.coeM t = Subtype.val '' t := by
sorry
This theorem states that for any type `α` and any set `s` of type `α`, if `t` is a set whose elements are subtypes of `s`, then the function `Lean.Internal.coeM` applied to `t` is equal to the set of values of `t`. In other words, it establishes an equivalence between the process of coercion via `Lean.Internal.coeM` and the set mapping operation that extracts the underlying values from the elements in `t`. The theorem thus connects two different ways to handle subtypes in Lean 4.
More concisely: For any type `α` and set `t` of subtypes of `α`, the application of `Lean.Internal.coeM` to `t` is equal to the set of underlying values of elements in `t`.
|