minimal_apply_mem_inter_range_iff

English

A minimal element relation with respect to a subset t via a mapping f and range condition is equivalent.

Русский

Минимум по отношению к подмножеству t через отображение f эквивалентен минимальному в диапазоне.

LaTeX

$$$\\forall f:\\, \\text{OrderEmbedding }\\alpha\\to\\beta,\\; \\text{Minimal}(\\cdot \\in t\\cap \\operatorname{range}f) (f x) \\iff \\text{Minimal}(f x \\in t) x$$$

Lean4

theorem minimal_apply_mem_inter_range_iff : Minimal (· ∈ t ∩ range f) (f x) ↔ Minimal (fun x ↦ f x ∈ t) x :=
  by
  refine ⟨fun h ↦ ⟨h.prop.1, fun y hy ↦ ?_⟩, fun h ↦ ⟨⟨h.prop, by simp⟩, ?_⟩⟩
  · rw [← f.le_iff_le, ← f.le_iff_le]
    exact h.le_of_le ⟨hy, by simp⟩
  rintro _ ⟨hyt, ⟨y, rfl⟩⟩
  simp_rw [f.le_iff_le]
  exact h.le_of_le hyt

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