antichain — Mathlib

English

From the exchange property, the encard of B1 \ B2 is at most the encard of B2 \ B1.

Русский

Из свойства обмена следует, что encard(B1 \ B2) ≤ encard(B2 \ B1).

LaTeX

$$$$ (B_1 \ B_2).encard \le (B_2 \ B_1).encard $$$$

Lean4

/-- A family of sets with the exchange property is an antichain. -/
theorem antichain (exch : ExchangeProperty IsBase) (hB : IsBase B) (hB' : IsBase B') (h : B ⊆ B') : B = B' :=
  h.antisymm
    (fun x hx ↦
      by_contra
        (fun hxB ↦
          let ⟨_, hy, _⟩ := exch B' B hB' hB x ⟨hx, hxB⟩;
          hy.2 <| h hy.1))

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