uIcc_subset_uIcc_iff_mem — Mathlib

English

An unordered interval [[a1, b1]] is contained in [[a2, b2]] precisely when a1 and b1 both lie in [[a2, b2]].

Русский

Неупорядоченный интервал [[a1, b1]] содержится в [[a2, b2]] тогда, когда оба конца a1 и b1 принадлежат [[a2, b2]].

LaTeX

$$$ [[a_1,b_1]] \\subseteq [[a_2,b_2]] \\iff a_1 \\in [[a_2,b_2]] \\land b_1 \\in [[a_2,b_2]] $$$

Lean4

theorem uIcc_subset_uIcc_iff_mem : [[a₁, b₁]] ⊆ [[a₂, b₂]] ↔ a₁ ∈ [[a₂, b₂]] ∧ b₁ ∈ [[a₂, b₂]] :=
  Iff.intro (fun h => ⟨h left_mem_uIcc, h right_mem_uIcc⟩) fun h => uIcc_subset_uIcc h.1 h.2

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