mem_lift'_sets — Mathlib

English

If h is monotone, then s ∈ f.lift' h iff there exists t ∈ f with h t ⊆ s.

Русский

Если h монотонно, то множество s принадлежит f.lift' h тогда и только тогда, существует t ∈ f такое, что h t ⊆ s.

LaTeX

$$$ (hh : Monotone h) \\Rightarrow (s \\in f.lift' h) \\iff \\exists t \\in f, h\\,t \\subseteq s $$$

Lean4

theorem mem_lift'_sets (hh : Monotone h) {s : Set β} : s ∈ f.lift' h ↔ ∃ t ∈ f, h t ⊆ s :=
  mem_lift_sets <| monotone_principal.comp hh

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