partialSups_disjointed — Mathlib

English

For a finite index set, the supremum over disjointed f equals the supremum over f.

Русский

Для конечного множителя индексов суперем над disjointed f равен суперему над f.

LaTeX

$$$[Fintype\ ι]\; (f: ι \to α)\quad univ.\;sup\; (disjointed f) = univ.\;sup\; f$$$

Lean4

@[simp]
theorem partialSups_disjointed (f : ι → α) : partialSups (disjointed f) = partialSups f := by
  -- This seems to be much more awkward than the case of linear orders, because the supremum
    -- in the definition of `disjointed` can involve multiple "paths" through the poset.
  classical
    -- We argue by induction on the size of `Iio i`.

  suffices ∀ r i (hi : #(Iio i) ≤ r), partialSups (disjointed f) i = partialSups f i from
    OrderHom.ext _ _ (funext fun i ↦ this _ i le_rfl)
  intro r i hi
  induction r generalizing i with
  | zero =>
    -- Base case: `n` is minimal, so `partialSups f i = partialSups (disjointed f) n = f i`.

    simp only [Nat.le_zero, card_eq_zero] at hi
    simp only [partialSups_apply, Iic_eq_cons_Iio, hi, disjointed_apply, sup'_eq_sup, sup_cons, sup_empty, sdiff_bot]
  | succ n ih =>
    -- Induction step: first WLOG arrange that `#(Iio i) = r + 1`

    rcases lt_or_eq_of_le hi with hn | hn
    · exact ih _ <| Nat.le_of_lt_succ hn
    simp only [partialSups_apply (disjointed f), Iic_eq_cons_Iio, sup'_eq_sup, sup_cons]
      -- Key claim: we can write `Iio i` as a union of (finitely many) `Ici` intervals.

    have hun : (Iio i).biUnion Iic = Iio i := by ext r;
      simpa using
        ⟨fun ⟨a, ha⟩ ↦ ha.2.trans_lt ha.1, fun hr ↦ ⟨r, hr, le_rfl⟩⟩
          -- Use claim and `sup_biUnion` to rewrite the supremum in the definition of `disjointed f`
              -- in terms of suprema over `Iic`'s. Then the RHS is a `sup` over `partialSups`, which we
              -- can rewrite via the induction hypothesis.

    rw [← hun, sup_biUnion, sup_congr rfl (g := partialSups f)]
    · simp only [funext (partialSups_apply f), sup'_eq_sup, ← sup_biUnion, hun]
      simp only [disjointed, sdiff_sup_self, Iic_eq_cons_Iio, sup_cons]
    · simp only [partialSups, sup'_eq_sup, OrderHom.coe_mk] at ih ⊢
      refine fun x hx ↦
        ih x
          ?_
            -- Remains to show `∀ x in Iio i, #(Iio x) ≤ r`.

      rw [← Nat.lt_add_one_iff, ← hn]
      apply lt_of_lt_of_le (b := #(Iic x))
      · simpa only [Iic_eq_cons_Iio, card_cons] using Nat.lt_succ_self _
      · refine card_le_card (fun r hr ↦ ?_)
        simp only [mem_Iic, mem_Iio] at hx hr ⊢
        exact hr.trans_lt hx

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