isCobounded_flip — Mathlib

English

If a filter f is bounded under a relation r, then it is cobounded under the flipped relation flip r.

Русский

Если фильтр f ограничен относительно отношения r, то он ограничен относительно отражённого отношения flip r с другой стороны (cobounded).

LaTeX

$$$\text{If } f \text{ is bounded under } r, \text{ then } f \text{ is cobounded under } (\text{flip } r).$$$

Lean4

/-- A filter which is eventually bounded is in particular frequently bounded (in the opposite
direction). At least if the filter is not trivial. -/
theorem isCobounded_flip [IsTrans α r] [NeBot f] : f.IsBounded r → f.IsCobounded (flip r)
  | ⟨a, ha⟩ =>
    ⟨a, fun b hb =>
      let ⟨_, rxa, rbx⟩ := (ha.and hb).exists
      show r b a from _root_.trans rbx rxa⟩

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