Theorems · Theorem · order theory

Set.image2_distrib_subset_left

∀ {α : Type u_1} {β : Type u_3} {β' : Type u_4} {γ : Type u_5} {γ' : Type u_6} {δ : Type u_7} {ε : Type u_9} {s : Set α}
  {t : Set β} {u : Set γ} {f : α → δ → ε} {g : β → γ → δ} {f₁ : α → β → β'} {f₂ : α → γ → γ'} {g' : β' → γ' → ε},
  (∀ (a : α) (b : β) (c : γ), f a (g b c) = g' (f₁ a b) (f₂ a c)) →
    Set.image2 f s (Set.image2 g t u) ⊆ Set.image2 g' (Set.image2 f₁ s t) (Set.image2 f₂ s u)

The other direction does not hold because of the s-s cross terms on the RHS.

Defined in

Mathlib.Data.Set.NAry

Cited by

5 results in Mathlib

Foundations

Depth 16 from the axioms · uses propext, Classical.choice, Quot.sound