le_of_codisjoint — Mathlib

English

If a and b are disjoint and b is codisjoint with c, then a ≤ c.

Русский

Если a и b дизъединены, и b кодиссоединено с c, тогда a ≤ c.

LaTeX

$$$\text{Disjoint}(a,b) \land \text{Codisjoint}(b,c) \rightarrow a \le c$$$

Lean4

theorem le_of_codisjoint (hab : Disjoint a b) (hbc : Codisjoint b c) : a ≤ c :=
  by
  rw [← @inf_top_eq _ _ _ a, ← @bot_sup_eq _ _ _ c, ← hab.eq_bot, ← hbc.eq_top, sup_inf_right]
  exact inf_le_inf_right _ le_sup_left

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