fin n has_Inf and has_Sup

Stream: new members

[Yakov Pechersky]

fin (n + 1) doesn't have has_Inf or has_Sup. I'm trying to crib the definitions from the definition of the instances for nat. Turns out fin.find is more general than nat.find and returns an option. RIght now I'm planning to use get_or_else with the following def. But I am not sure how to show the decidability. Thoughts?

noncomputable instance {n : ℕ} : has_Inf (fin (n + 1)) :=
⟨λ s, option.get_or_else (fin.find (λ n, n ∈ s ∧ ∀ m < n, m ∉ s)) 0

[Mario Carneiro]

There should be a general lemma saying that a finite linear order is complete

[Mario Carneiro]

actually a finite lattice is good enough

[Mario Carneiro]

actually a bot_join_semilattice also works

[Mario Carneiro]

the proof is pretty easy: every Sup is a finite fold of join and bot, so Sup exists, and therefore all the complete lattice operations exist

[Yakov Pechersky]

I mean the infimum of a set, not the infimum of two sets. has_Inf is the former, has_inf is the latter. I think? Am I wrong?

[Mario Carneiro]

Yes, that's correct. The observation is that binary infima give you arbitrary infima if there are only finitely many objects in the type

[Kevin Buzzard]

inf is just min in this context, it's the inf of two terms of the lattice (so two numbers, not two sets)

[Reid Barton]

You mean not the infimum of two elements, not not the infimum of two sets. :upside_down:

[Mario Carneiro]

Also for your question re: decidability, don't worry about it and use open_locale classical. It is impossible to implement has_Inf computably on any type where this is actually a useful thing to say

[Yakov Pechersky]

Gotcha. Thanks! So what would be the right way to state that the following using min?

(leading : ∀ i : fin n, A i (Inf {j : fin m | A i j ≠ 0}) = 1)

[Mario Carneiro]

One way to do it with fin.find is to assert that fin.find ... = some j and then say A i j = 1

[Mario Carneiro]

or assert that for all j satisfying that, A i j = 1

[Reid Barton]

maybe nothing like this at all, but rather say that if A i j is nonzero but all A i j' with j' < j are zero, then A i j is one

[Mario Carneiro]

depending on whether you want to assert the existence of such a value or not

[Mario Carneiro]

or what Reid said

[Reid Barton]

and yeah I guess this might not be exactly equivalent to what you wrote

[Mario Carneiro]

The version you wrote seems to require that A i j is not always zero, in which case you can write it as "there exists j such that A i j = 1 and A i j' = 0 for all j' < j"

[Mario Carneiro]

assuming of course that 0 != 1

[Yakov Pechersky]

Yeah, I had those definitions before, but was testing out what the argmin equivalent would be. Which led me to try creating a has_Inf instance.

[Yakov Pechersky]

(leading : ∀ i : fin n, (∃ j : fin m, A i j = 1 → ∀ lj : fin m, lj < j → A i lj = 0) )

[Mario Carneiro]

(leading : ∀ i : fin n, (∃ j : fin m, A i j = 1 /\ ∀ lj : fin m, lj < j → A i lj = 0) )

[Yakov Pechersky]

But doesn't that preclude an all-zero row?

[Mario Carneiro]

it does

[Mario Carneiro]

do you want to allow that?

[Mario Carneiro]

if so:

(leading : ∀ i : fin n, (∀ j : fin m, (∀ lj : fin m, lj < j → A i lj = 0) -> A i j != 0 -> A i j = 1)

[Yakov Pechersky]

(leading : ∀ i : fin n, (∃ j : fin m, A i j = 1) → (∃ j : fin m, ∀ lj : fin m, lj < j → A i j = 1 ∧ A i lj = 0) )

[Mario Carneiro]

ah, putting A i j = 1 ∧ in the final conjunct is a bit weird in case there is no such lj

[Mario Carneiro]

also your definition would still hold if every element was 0.5 say

[Yakov Pechersky]

I see. Thanks! I'm trying to formalize the definition of reduced-row-echelon form, with the hope to also formalize an algorithm for converting a matrix to it, if possible.