disjSups_assoc — Mathlib

English

For all Finsets s,t,u, (s ○ t) ○ u = s ○ (t ○ u).

Русский

Для любых конечных множеств s,t,u выполняется (s ○ t) ○ u = s ○ (t ○ u).

LaTeX

$$$ (s \\circ t) \\circ u = s \\circ (t \\circ u) $$$

Lean4

theorem disjSups_assoc : ∀ s t u : Finset α, s ○ t ○ u = s ○ (t ○ u) :=
  by
  refine (associative_of_commutative_of_le inferInstance ?_).assoc
  simp only [le_eq_subset, disjSups_subset_iff, mem_disjSups]
  rintro s t u _ ⟨a, ha, b, hb, hab, rfl⟩ c hc habc
  rw [disjoint_sup_left] at habc
  exact ⟨a, ha, _, ⟨b, hb, c, hc, habc.2, rfl⟩, hab.sup_right habc.1, (sup_assoc ..).symm⟩

Похожие утверждения