theorem
Set.image2_def
{α : Type u_1}
{β : Type u_1}
{γ : Type u_1}
(f : α → β → γ)
(s : Set α)
(t : Set β)
:
Set.image2 f s t = Seq.seq (f <$> s) fun x => t
Set.image2 in terms of monadic operations. Note that this can't be taken as the definition
because of the lack of universe polymorphism.
Equations
- Set.instAlternativeSet = let src := Set.monad; Alternative.mk (fun {α} => ∅) fun {α} s t => s ∪ t ()
Monadic coercion lemmas #
theorem
Set.mem_coe_of_mem
{α : Type u}
{β : Set α}
{γ : Set ↑β}
{a : α}
(ha : a ∈ β)
(ha' : { val := a, property := ha } ∈ γ)
:
a ∈ Lean.Internal.coeM γ
theorem
Set.mem_of_mem_coe
{α : Type u}
{β : Set α}
{γ : Set ↑β}
{a : α}
(ha : a ∈ Lean.Internal.coeM γ)
:
theorem
Set.eq_univ_of_coe_eq
{α : Type u}
{β : Set α}
{γ : Set ↑β}
(hγ : Lean.Internal.coeM γ = β)
:
γ = Set.univ
theorem
Set.image_coe_eq_restrict_image
{α : Type u}
{β : Set α}
{γ : Set ↑β}
{δ : Type u_1}
{f : α → δ}
:
f '' Lean.Internal.coeM γ = Set.restrict β f '' γ