inf'_union — Mathlib

English

For nonempty Finsets s1, s2, the infimum over s1 ∪ s2 equals the meet of the infima over s1 and s2: inf'_{s1∪s2} f = inf'(s1) f ⊓ inf'(s2) f.

Русский

Для непустых Finset s1, s2 инфимум над объединением равен meet инфимумов поштос: inf' over s1∪s2 = inf's1 f ⊓ inf's2 f.

LaTeX

$$$ (s_1 \\cup s_2).inf' (h_1.mono \\text{subset\_left}) f = s_1.inf' h_1 f \\inf s_2.inf' h_2 f $$$

Lean4

theorem inf'_union [DecidableEq β] {s₁ s₂ : Finset β} (h₁ : s₁.Nonempty) (h₂ : s₂.Nonempty) (f : β → α) :
    (s₁ ∪ s₂).inf' (h₁.mono subset_union_left) f = s₁.inf' h₁ f ⊓ s₂.inf' h₂ f :=
  @sup'_union αᵒᵈ _ _ _ _ _ h₁ h₂ _

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