map_inl_inf_map_inr — Mathlib

English

The infimum of the two pushforwards map inl f and map inr g is the bottom filter: they are disjoint in a precise sense.

Русский

Нижняя граница двух образов map inl f и map inr g равна нулю фильтру: они несовместимы в точном смысле.

LaTeX

$$@[simp] theorem map_inl_inf_map_inr : map inl f ⊓ map inr g = ⊥$$

Lean4

@[simp]
theorem map_inl_inf_map_inr : map inl f ⊓ map inr g = ⊥ :=
  by
  apply le_bot_iff.mp
  trans map inl ⊤ ⊓ map inr ⊤
  · apply inf_le_inf <;> simp
  · simp

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