coe_inf — Mathlib

English

The underlying set of the infimum I ⊓ J equals the intersection of the underlying sets: ↑(I ⊓ J) = I ∩ J.

Русский

Подмножество нижнего предела I ⊓ J равно пересечению соответствующих множеств: ↑(I ⊓ J) = I ∩ J.

LaTeX

$$$\uparrow(I \inf J) = \uparrow I \cap J$$$

Lean4

@[simp]
theorem coe_inf (I J : WithBot (Box ι)) : (↑(I ⊓ J) : Set (ι → ℝ)) = (I : Set _) ∩ J :=
  by
  induction I
  · change ∅ = _
    simp
  induction J
  · change ∅ = _
    simp
  change ((mk' _ _ : WithBot (Box ι)) : Set (ι → ℝ)) = _
  simp only [coe_eq_pi, ← pi_inter_distrib, Ioc_inter_Ioc, Pi.sup_apply, Pi.inf_apply, coe_mk', coe_coe]

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