mem_lift_sets — Mathlib

English

If g is monotone, then membership in f.lift g is equivalent to the existence of a t ∈ f with s ∈ g t.

Русский

Если g монотонна, то членство в f.lift g эквивалентно существованию t ∈ f такое, что s ∈ g t.

LaTeX

$$$s \\in f.lift g \\iff \\exists t \\in f, s \\in g t$$$

Lean4

theorem mem_lift_sets (hg : Monotone g) {s : Set β} : s ∈ f.lift g ↔ ∃ t ∈ f, s ∈ g t :=
  (f.basis_sets.mem_lift_iff (fun s => (g s).basis_sets) hg).trans <| by simp only [id, exists_mem_subset_iff]

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