Theorems · Theorem · order theory

Set.InvOn.prodMap

∀ {α₁ : Type u_7} {α₂ : Type u_8} {β₁ : Type u_9} {β₂ : Type u_10} {s₁ : Set α₁} {s₂ : Set α₂} {t₁ : Set β₁}
  {t₂ : Set β₂} {f₁ : α₁ → β₁} {f₂ : α₂ → β₂} {g₁ : β₁ → α₁} {g₂ : β₂ → α₂},
  Set.InvOn g₁ f₁ s₁ t₁ →
    Set.InvOn g₂ f₂ s₂ t₂ → Set.InvOn (fun x => (g₁ x.1, g₂ x.2)) (fun x => (f₁ x.1, f₂ x.2)) (s₁ ×ˢ s₂) (t₁ ×ˢ t₂)

Defined in

Mathlib.Data.Set.Function

Cited by

2 results in Mathlib

Foundations

Depth 7 from the axioms · uses no axioms