piecewise_mem_Icc' — Mathlib

English

If f1 and f2 both belong to Icc(g1,g2), then s.piecewise f1 f2 belongs to Icc g1 g2.

Русский

Если f1 и f2 принадлежат Icc(g1,g2), то s.piecewise f1 f2 принадлежит Icc g1 g2.

LaTeX

$$$$ s.piecewise\; f_1\; f_2 \in Icc(g_1,g_2) $$$$

Lean4

theorem piecewise_mem_Icc' {s : Set ι} [∀ j, Decidable (j ∈ s)] {f₁ f₂ g₁ g₂ : ∀ i, α i} (h₁ : f₁ ∈ Icc g₁ g₂)
    (h₂ : f₂ ∈ Icc g₁ g₂) : s.piecewise f₁ f₂ ∈ Icc g₁ g₂ :=
  piecewise_mem_Icc (fun _ _ ↦ ⟨h₁.1 _, h₁.2 _⟩) fun _ _ ↦ ⟨h₂.1 _, h₂.2 _⟩

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