forall_uIoc_iff — Mathlib

English

For any P, if P holds for all x in I a,b then P holds for all x in I a,b and I b,a together.

Русский

Для любого P: если P выполняется для всех x в I(a,b), тогда P выполняется и для всех x в I(a,b) и в I(b,a).

LaTeX

$$$ \\forall P:\\alpha \\to \\mathrm{Prop},\\ (\\forall x\\in Ι(a,b),\\ P(x)) \\iff (\\forall x\\in Ioc(a,b),\\ P(x)) \\land (\\forall x\\in Ioc(b,a),\\ P(x)) $$$

Lean4

theorem forall_uIoc_iff {P : α → Prop} : (∀ x ∈ Ι a b, P x) ↔ (∀ x ∈ Ioc a b, P x) ∧ ∀ x ∈ Ioc b a, P x := by
  simp only [uIoc_eq_union, mem_union, or_imp, forall_and]

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