English
See previous item.
Русский
См. предыдущий пункт.
LaTeX
$$$\text{Induction on } \mathrm{latticeClosure}(s)$$$
Lean4
theorem latticeClosure_sup_inf_induction (p : (a : α) → a ∈ latticeClosure s → Prop)
(mem : ∀ (a : α) (has : a ∈ s), p a (subset_latticeClosure has))
(sup :
∀ (a : α) (has : a ∈ latticeClosure s) (b : α) (hbs : b ∈ latticeClosure s),
p a has → p b hbs → p (a ⊔ b) (isSublattice_latticeClosure.supClosed has hbs))
(inf :
∀ (a : α) (has : a ∈ latticeClosure s) (b : α) (hbs : b ∈ latticeClosure s),
p a has → p b hbs → p (a ⊓ b) (isSublattice_latticeClosure.infClosed has hbs))
{a : α} (has : a ∈ latticeClosure s) : p a has :=
by
have h : IsSublattice {a : α | ∃ has : a ∈ latticeClosure s, p a has} :=
{ supClosed := fun a ⟨has, hpa⟩ b ⟨hbs, hpb⟩ =>
⟨isSublattice_latticeClosure.supClosed has hbs, sup a has b hbs hpa hpb⟩
infClosed := fun a ⟨has, hpa⟩ b ⟨hbs, hpb⟩ =>
⟨isSublattice_latticeClosure.infClosed has hbs, inf a has b hbs hpa hpb⟩ }
refine (latticeClosure_min (fun a ha ↦ ?_) h has).choose_spec
exact ⟨subset_latticeClosure ha, mem a ha⟩
