absorbs_inter — Mathlib

English

If hs and ht are both absorptions by u, then their intersection s ∩ t is absorbed by u.

Русский

Если hs и ht обе поглощают u, то s ∩ t поглощает u.

LaTeX

$$$Absorbs G_0 (s \cap t) u \leftrightarrow Absorbs G_0 s u \land Absorbs G_0 t u$$$

Lean4

@[simp]
theorem absorbs_inter : Absorbs G₀ (s ∩ t) u ↔ Absorbs G₀ s u ∧ Absorbs G₀ t u := by
  simp only [absorbs_iff_eventually_cobounded_mapsTo, mapsTo_inter, eventually_and]

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