English
For boxes I,J, the following four conditions are equivalent: I ≤ J; the ambient set inclusion; Icc(I.lower,I.upper) ⊆ Icc(J.lower,J.upper); and J.lower ≤ I.lower and I.upper ≤ J.upper.
Русский
Для коробок I,J следующие четыре условия эквивалентны: I ≤ J; включение подмножества в окружении; Icc(I.lower,I.upper) ⊆ Icc(J.lower,J.upper); и J.lower ≤ I.lower и I.upper ≤ J.upper.
LaTeX
$$$ (I \\le J) \\iff \\Bigl( (I : Set (ι \\to ℝ)) \\subseteq J \\Bigr) \\iff \\Bigl( \\mathrm{Icc}(I.lower,I.upper) \\subseteq \\mathrm{Icc}(J.lower,J.upper) \\Bigr) \\iff \\Bigl( J.lower \\le I.lower \\land I.upper \\le J.upper \\Bigr) $$$
Lean4
theorem le_TFAE :
List.TFAE
[I ≤ J, (I : Set (ι → ℝ)) ⊆ J, Icc I.lower I.upper ⊆ Icc J.lower J.upper,
J.lower ≤ I.lower ∧ I.upper ≤ J.upper] :=
by
tfae_have 1 ↔ 2 := Iff.rfl
tfae_have 2 → 3
| h => by simpa [coe_eq_pi, closure_pi_set, lower_ne_upper] using closure_mono h
tfae_have 3 ↔ 4 := Icc_subset_Icc_iff I.lower_le_upper
tfae_have 4 → 2
| h, x, hx, i => Ioc_subset_Ioc (h.1 i) (h.2 i) (hx i)
tfae_finish
