Commit 2022-05-07 15:50 51667657

chore(order/filter/pointwise): Better definitional unfolding (#13941) Tweak pointwise operation definitions to make them easier to work with:

• 1 is now pure 1 instead of principal 1. This changes defeq.
• Binary operations unfold to the set operation instead exposing a bare set.image2 (obtain ⟨t₁, t₂, h₁, h₂, h⟩ : s ∈ f * g now gives h : t₁ * t₂ ⊆ s instead of h : set.image2 (*) t₁ t₂ ⊆ s. This does not change defeq.