Theorems · Theorem · order theory

Set.seq_seq

∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set (β → γ)} {t : Set (α → β)} {u : Set α},
  s.seq (t.seq u) = (((fun x1 x2 => x1 ∘ x2) '' s).seq t).seq u

Defined in

Mathlib.Data.Set.Lattice.Image

Cited by

1 results in Mathlib

Foundations

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