withBotCoe_subset_iff — Mathlib

English

For any boxes I,J, the inclusion of their underlying sets corresponds to the box order: (I as set) ⊆ J iff I ≤ J.

Русский

Для любых коробок I, J включение соответствующих множеств (I как множество) ⊆ J эквивалентно отношению I ≤ J в порядке коробок.

LaTeX

$$$(I : Set (ι \to \mathbb{R})) \subseteq J \ \iff \ I \le J$$$

Lean4

@[simp, norm_cast]
theorem withBotCoe_subset_iff {I J : WithBot (Box ι)} : (I : Set (ι → ℝ)) ⊆ J ↔ I ≤ J :=
  by
  induction I; · simp
  induction J; · simp [subset_empty_iff]
  simp [le_def]

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