English
The set product s ×ˢ t is equivalent to the type product s.Elem × t.Elem, i.e., the set-theoretic product corresponds to the cartesian product of the subtypes.
Русский
Произведение множеств s ×ˢ t эквивалентно обычному произведению подтипов s.Elem × t.Elem, то есть множество-образ произвдённого соответствует декартову произведению подмножеств.
LaTeX
$$Equiv (Set.instSProd.sprod s t).Elem (Prod s.Elem t.Elem)$$
Lean4
/-- The set product of two sets is equivalent to the type product of their coercions to types. -/
protected def prod {α β} (s : Set α) (t : Set β) : ↥(s ×ˢ t) ≃ s × t :=
@subtypeProdEquivProd α β s t
