prodMk — Mathlib

English

If hD ensures that {a,b} ∈ D whenever a ≤ b, and f,g are Scott-continuous on D, then x ↦ (f x, g x) is Scott-continuous on D.

Русский

Если для любых a ≤ b множество {a,b} принадлежит D и f,g — Scott–непрерывны на D, то x ↦ (f x, g x) Scott–непрерывна на D.

LaTeX

$$$(\\forall a b, a \\le b \\to {a,b} \\in D) \\to \\mathrm{ScottContinuousOn}(D,f) \\to \\mathrm{ScottContinuousOn}(D,g) \\to \\mathrm{ScottContinuousOn}(D,\\lambda x.(f x,g x)).$$$

Lean4

theorem prodMk (hD : ∀ a b : α, a ≤ b → { a, b } ∈ D) (hf : ScottContinuousOn D f) (hg : ScottContinuousOn D g) :
    ScottContinuousOn D fun x => (f x, g x) := fun d hd₁ hd₂ hd₃ a hda =>
  by
  rw [IsLUB, IsLeast, upperBounds]
  constructor
  · simp only [mem_image, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂, mem_setOf_eq, Prod.mk_le_mk]
    intro b hb
    exact ⟨hf.monotone D hD (hda.1 hb), hg.monotone D hD (hda.1 hb)⟩
  · intro ⟨p₁, p₂⟩ hp
    simp only [mem_image, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂, mem_setOf_eq, Prod.mk_le_mk] at hp
    constructor
    · rw [isLUB_le_iff (hf hd₁ hd₂ hd₃ hda), upperBounds]
      simp only [mem_image, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂, mem_setOf_eq]
      intro _ hb
      exact (hp _ hb).1
    · rw [isLUB_le_iff (hg hd₁ hd₂ hd₃ hda), upperBounds]
      simp only [mem_image, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂, mem_setOf_eq]
      intro _ hb
      exact (hp _ hb).2

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