disjoint_sSup — Mathlib

English

If sSupIndep s, then for any x ∈ s and y ⊆ s with x ∉ y, Disjoint x (sSup y).

Русский

Если sSupIndep s, то для любого x ∈ s и y ⊆ s с x ∉ y выполняется Disjoint x (sSup y).

LaTeX

$$sSupIndep s → ∀ x ∈ s, ∀ y ⊆ s, x ∉ y → Disjoint x (sSup y)$$

Lean4

/-- If the elements of a set are independent, then any element is disjoint from the `sSup` of some
subset of the rest. -/
theorem disjoint_sSup {x : α} {y : Set α} (hx : x ∈ s) (hy : y ⊆ s) (hxy : x ∉ y) : Disjoint x (sSup y) :=
  by
  have := (hs.mono <| insert_subset_iff.mpr ⟨hx, hy⟩) (mem_insert x _)
  rw [insert_diff_of_mem _ (mem_singleton _), diff_singleton_eq_self hxy] at this
  exact this

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