instMaxOfSemilatticeSup — Mathlib

English

If Y has a semilattice supremum and zero, then LocallyFinsuppWithin forms a Max object where (D1 ∨ D2)(x) = max(D1(x), D2(x)) for all x.

Русский

Если у Y есть полуполу верхняя граница (Max), то LocallyFinsuppWithin образует структуру Max, где (D1 ∨ D2)(x) = max(D1(x), D2(x)).

LaTeX

$$$\\max(D_1, D_2) \\;:\\; X \\to Y\\quad (\\max(D_1, D_2))(x) = \\max(D_1(x), D_2(x))$$$

Lean4

instance [SemilatticeSup Y] [Zero Y] : Max (locallyFinsuppWithin U Y) where
  max D₁
    D₂ :=
    { toFun z := max (D₁ z) (D₂ z)
      supportWithinDomain' := by
        intro x
        contrapose
        intro hx
        simp [notMem_support.1 fun a ↦ hx (D₁.supportWithinDomain a),
          notMem_support.1 fun a ↦ hx (D₂.supportWithinDomain a)]
      supportLocallyFiniteWithinDomain' := by
        intro z hz
        obtain ⟨t₁, ht₁⟩ := D₁.supportLocallyFiniteWithinDomain z hz
        obtain ⟨t₂, ht₂⟩ := D₂.supportLocallyFiniteWithinDomain z hz
        use t₁ ∩ t₂, inter_mem ht₁.1 ht₂.1
        apply Set.Finite.subset (s := (t₁ ∩ D₁.support) ∪ (t₂ ∩ D₂.support)) (ht₁.2.union ht₂.2)
        intro a ha
        simp_all only [mem_inter_iff, mem_support, ne_eq, mem_union, true_and]
        by_contra hCon
        push_neg at hCon
        simp_all }

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