le_egauge_inter — Mathlib

English

The egauge of a union is bounded by the infimum of egauges over the components; specifically, egauge(s) ⊔ egauge(t) ≤ egauge(s ∩ t).

Русский

Гейдж объединения не превосходит максимум гейджей компонентов: egauge(s) ⊔ egauge(t) ≤ egauge(s ∩ t).

LaTeX

$$$\mathrm{egauge}_{\mathbb{K}}(s,x) \sqcup \mathrm{egauge}_{\mathbb{K}}(t,x) \le \mathrm{egauge}_{\mathbb{K}}(s \cap t, x)$$$

Lean4

theorem le_egauge_inter (s t : Set E) (x : E) : egauge 𝕜 s x ⊔ egauge 𝕜 t x ≤ egauge 𝕜 (s ∩ t) x :=
  max_le (egauge_anti _ inter_subset_left _) (egauge_anti _ inter_subset_right _)

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